IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
preserved by star112111 1. T : Type
2. P : TProp
3. R : TTProp
4. x,y:T. P(x) (xRy) P(y)
5. n : 6. 0<n 7. n-10 (x,y:T. P(x) (xR^n-1 y) P(y))
8. n0
9. x : T 10. y : T 11. P(x)
12. n = 0
13. z : T 14. xRz 15. zR^n-1 y 16. P(z)
P(y)
By:
Using [`x',z] BackThruSomeHyp
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html