(23steps total) PrintForm Definitions hol prim rec Sections HOLlib Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: hless def 1 1
1. m : 
2. n : 
3. m<n
  P:(). (n:. P(n+1)  P(n)) & P(m) & P(n)
By: DTerm (m.m<n) 0 THEN Simp THEN StrongAuto

Generated subgoals:

None

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

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