(8steps total) PrintForm Definitions hol prim rec Sections HOLlib Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: hpre def 1 2
1. m : 
2. m = 0
  m-1 = if m = 0 then 0 else @n:. (m = (n+1)) fi 
By: Subst ((m = 0) = false) 0 THEN Simp THEN StrongAuto

Generated subgoals:

1   m = 0  
2 steps
2   m-1 = (@n:. (m = (n+1)))
2 steps

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

(8steps total) PrintForm Definitions hol prim rec Sections HOLlib Doc