Intuitionize soeq1 in iset.mm
Intuitionize soeq1 in iset.mm

The proof is a fairly straightforward update to work the same
way but reflect the differences between df-so and df-iso .

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