1. n : 
2. 0<n
3. T:Type, R1,R2:(TTProp).
3. (x,y:T. (x R1 y)  (x R2 y))  (x,y:T. (x R1^n-1 y)  (x R2^n-1 y))
4. T : Type
5. R1 : TTProp
6. R2 : TTProp
7. x,y:T. (x R1 y)  (x R2 y)
8. n = 0
9. x : T
10. y : T
11. z:T. (x R1 z) & (z R1^n-1 y)
  z:T. (x R2 z) & (z R2^n-1 y)

None

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