(2steps total) PrintForm Definitions hol sum Sections HOLlib Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: houtl nuprl 1
1. 'a : S
2. 'b : S
3. u : 'a+'b
4. isl(u)
  outl(u) = outl(u)
By: Unab [`houtl`] THEN Analyze 3 THEN Simp THEN StrongAuto

Generated subgoals:

None

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

(2steps total) PrintForm Definitions hol sum Sections HOLlib Doc