IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
rel star of equiv1 1. T : Type
2. E : TTProp
3. x : T 4. y : T 5. EquivRel(T)(_1 E _2)
6. n :
7. xE^ny xEy
By:
MoveToConcl -1 THEN MoveToConcl 4 THEN MoveToConcl 3 THEN MoveToConcl -1
THEN
InductionOnNat