Nuprl - Proof: harb wd 1 1 1 1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: harb wd 1 1 1 1 1

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

{x:'a| True })

{x:'a| True } = 'a

{'a:S}

By:	Analyze 3 THEN Try (Analyze 0 THEN Complete Auto)

Generated subgoal:

1 3. {x:'a| True } = 'a Type
{x:'a| True } = 'a {'a:S}
1 step

About:

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html