1. T : Type
2. E : TTProp
3. EquivRel x,y:T. E(x,y)
4. f : TT
5. x,y:T. (x f y)  E(x,y)
6. f  (x,y:T//E(x,y))(x,y:T//E(x,y))
7. u : x,y:T//E(x,y)
8. v : x,y:T//E(x,y)
  ((u f v)  u = v)

1

7. v1 : T 8. v2 : T 9. E(v1,v2) 10. u1 : T 11. u2 : T 12. E(u1,u2)   * = *  ((u1 f v1)  u1 = v1  x,y:T//E(x,y))

5 steps

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