IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
comp nat ind tp111213 1. P : Prop
2. i:. (j:. j<iP(j)) P(i)
3. 4. i1 : (0i1) Type{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)) 
(0
i1) 
Type{1}
