(4steps total) PrintForm Definitions hol arithmetic 1 Sections HOLlib Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: exp wf 1 1

1. m : 
  exp(m;0)  


By: RecUnfold `exp` 0 THEN RepeatFor 2 Simp


Generated subgoals:

None

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

(4steps total) PrintForm Definitions hol arithmetic 1 Sections HOLlib Doc