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

By:	Inst Thm* A = B  A  B & B  A [lexpr{1};{x:'a| True };'a] THEN StrongAuto

1

2. {x:'a| True } = 'a  Type  {x:'a| True }  'a & 'a  {x:'a| True } 3. ({x:'a| True } = 'a  Type)  ({x:'a| True }  'a & 'a  {x:'a| True })   {x:'a| True } = 'a  {'a:S}

2 steps

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