(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 2
1. 'a : S
  arb('a) = InjCase(lem('a); x. x, arb('a))
By: Unab [`arb`] THEN GenDC (lem('a)) THEN StrongAuto

Generated subgoal:

1 2. 'aVoid
  "uu" = "uu"  'a
2 steps

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