Nuprl - hol_arithmetic_4 LEMMAs for gen

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

Theorem	Name
Thm* P:(). P(0) & (n:. (m:. m<n P(m)) P(n)) (n:. P(n))	[gen_induction]
cites the following:
Thm* all Thm* (P:hnum hbool. implies Thm* (P:hnum hbool. (and Thm* (P:hnum hbool. ((P(0) Thm* (P:hnum hbool. (,all Thm* (P:hnum hbool. (,(n:hnum. implies Thm* (P:hnum hbool. (,(n:hnum. (all(m:hnum. implies(lt(m,n),P(m))) Thm* (P:hnum hbool. (,(n:hnum. ,P(n)))) Thm* (P:hnum hbool. ,all(n:hnum. P(n))))	[hgen_induction]

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