PrintForm Definitions hol sum Sections HOLlib Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: houtr nuprl
  'a,'b:S, u:'a+'b. isr(u)  outr(u) = outr(u)
By: Id THEN StrongAuto THEN Unab [`houtr`] THEN Analyze 3 THEN Simp THEN StrongAuto

Generated subgoals:

None

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

PrintForm Definitions hol sum Sections HOLlib Doc