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
  x,y@0:T. (x (x,y. z:T. (x E z) & (z E^n-1 y)) y@0)  (x E y@0)

1

8. x : T 9. y@0 : T 10. z:T. (x E z) & (z E^n-1 y@0)   x E y@0

2 steps

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