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)
  x,y:T. (x E^n y)  (x E y)

1	7. n = 0   x@0,y:T. (x@0 (x,y. x = y) y)  (x@0 E y)	Auto
2	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)	3 steps

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