PrintForm Definitions hol prim rec Sections HOLlib Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: hsimp rec rel wf
  'a:S. simp_rec_rel  ((hnum  'a)  'a  ('a  'a)  hnum  hbool)
By: HN THEN Simp THEN StrongAuto THEN Unfolds [`hsimp_rec_rel`] 0

Generated subgoals:

None

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

PrintForm Definitions hol prim rec Sections HOLlib Doc