T:Type, E:(TTProp), x,y:T.
  EquivRel(T)(_1 E _2)  (x (E^*) y)  (x E y)

1

1. T : Type 2. E : TTProp 3. x : T 4. y : T 5. EquivRel(T)(_1 E _2) 6. n :  7. x E^n y   x E y

8 steps

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