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