IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
comp nat ind tp11111122 1. P : Prop
2. i:. (j:. j<iP(j)) P(i)
3. zz : 4. 0<zz 5. i:. i<zz-1 P(i)
6. i : (i<zz) Prop{1}
By:
MemEqCD THEN MemEqCD
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Prop
i:
P(j)) 
(i<zz) 
Prop{1}
