(2steps total) PrintForm Definitions hol num Sections HOLlib Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: hzero rep def
  equal(zero_rep,select(x:hind. all(y:hind. not(equal(x,suc_rep(y))))))
By: HN THEN StrongAuto THEN Unab [`hzero_rep`] THEN HN THEN StrongAuto

Generated subgoal:

1   (@x:. (y:. x = suc_rep(y)  )) = (@x:. (y:. (x = (suc_rep(y)))))
1 step

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

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