1. T : Type
2. E : TTProp
3. EquivRel(T)(_1 E _2)
4. n : 
5. 0<n
6. x,y:T. (x E^n-1 y)  (x E y)
7. n = 0
8. x : T
9. y@0 : T
10. z:T. (x E z) & (z E^n-1 y@0)
  x E y@0

1

3. Refl(T)(_1 E _2) 4. Sym _1,_2:T. _1 E _2 5. Trans x,y:T. x E y 6. n :  7. 0<n 8. x,y:T. (x E^n-1 y)  (x E y) 9. n = 0 10. x : T 11. y@0 : T 12. z : T 13. x E z 14. z E^n-1 y@0   z E y@0

1 step

About: IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html