Intuitionize shftdm in iset.mm
Intuitionize shftdm in iset.mm

The statement of the theorem does not change; the proof has some minor
changes related to differences in ovex and related steps.

metamath/set.mm,metamath/set.mm,metamath/set.mm