PrintForm Definitions hol sum Sections HOLlib Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: hisr wd
  'a,'b:S. and(all(x:'b. isr(inr(x))),all(y:'a. not(isr(inl(y)))))
By: Unab [`hisr`] THEN HN THEN StrongAuto THEN Try (Complete (Unfold `label` 0))

Generated subgoals:

None

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

PrintForm Definitions hol sum Sections HOLlib Doc