IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
choose unique11 1. 'a : Type
2. P : 'aType
3. x : 'a 4. P(x)
5. y:'a. P(y) x = y 6. x2 : {y:'a| P(y) }
x2 = x
By:
Analyze 6 THEN InstHyp [x2] 5 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
x2 = x
