IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
choose true121 1. 'a : Type
2. P : 'aProp
3. x : 'a 4. P(x)
5. {x:'a| P(x) }Void
{x:'a| P(x) }
By:
DTerm x 0
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Prop
{x:'a| P(x) }
