IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
rel exp wf1 1. n : 2. 0<n 3. T:Type, R:(TTProp). R^n-1 TTProp
4. n = 0
5. T : Type
6. R : TTProp
7. T 8. y : T 9. z : T (zR^n-1 y) Prop
By:
InstHyp [T;R] 3
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
T:Type, R:(T
T
T
n = 0
(z R^n-1 y) 
