(13steps total) PrintForm Definitions Lemmas hol restr binder Sections HOLlib Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: harb wd 1 1 1
1. 'a : S
  arb('a) = InjCase(lem({x:'a| True }); x. x, arb('a))
By: Subst ({x:'a| True } = 'a) 0 THEN StrongAuto

Generated subgoals:

1   {x:'a| True } = 'a  {'a:S}
3 steps
2   arb('a) = InjCase(lem('a); x. x, arb('a))
3 steps
3 2. z : {'a:S}
  z  Type
1 step
4 2. z : {'a:S}
3. x : z
4. lem(z) = inl(x)
  x  'a
2 steps

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

(13steps total) PrintForm Definitions Lemmas hol restr binder Sections HOLlib Doc