(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 4
1. 'a : S
2. z : {'a:S}
3. x : z
4. lem(z) = inl(x)
  x  'a
By: Analyze 2 THEN StrongAuto

Generated subgoal:

1 2. z : S
3. z = 'a
4. x : z
5. lem(z) = inl(x)
  x  'a
1 step

About:
voidunioninlapplyfunctionequalmember
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