1. T : Type
2. E : TTProp
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

None

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