IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
sfa doc void rectype11 1. Q : rec(A.A)Prop
2. X:{X:rec(A.A)| Q(X) }. X Void
3. X : {X:rec(A.A)| Q(X) }
X Void
By:
BackThru: Hyp:-2
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html