IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
harb wd111111 1. 'a : S
2. {x:'a| True } = 'a {x:'a| True } 'a & 'a {x:'a| True }
3. {x:'a| True } = 'a {x:'a| True } = 'a {'a:S}
By:
Analyze THEN Try (Complete Auto) THEN Analyze 1 THEN Unhide THEN Analyze
THEN
Try (Complete Auto)
THEN
ParallelOp 2
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
{x:'a| True } 
'a & 'a 
{x:'a| True } = 'a 
{'a:S}
