(2steps total) PrintForm Definitions hol arithmetic 2 Sections HOLlib Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: hodd wd
  and(equal(odd(0),f),all(n:hnum. equal(odd(suc(n)),not(odd(n)))))
By: HN THEN Simpsetp [`nlogic`]

Generated subgoal:

1 1. n : 
  odd(n+1) = odd(n)
1 step

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

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