---

Step * of Lemma complete-nat-induction-ext

∀[P:ℕ ⟶ ℙ]. ((∀n:ℕ. ((∀m:ℕn. P[m]) ⇒ P[n])) ⇒ (∀n:ℕ. P[n]))
BY
{ Extract of Obid: complete-nat-induction
  normalizes to:
  
  λF.letrec rec(n)=F n rec in
      rec 
  finishing with (RepUR ``genrec so_apply`` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[P:\mBbbN{}  {}\mrightarrow{}  \mBbbP{}].  ((\mforall{}n:\mBbbN{}.  ((\mforall{}m:\mBbbN{}n.  P[m])  {}\mRightarrow{}  P[n]))  {}\mRightarrow{}  (\mforall{}n:\mBbbN{}.  P[n]))


By

---

Latex:
Extract  of  Obid:  complete-nat-induction
normalizes  to:

\mlambda{}F.letrec  rec(n)=F  n  rec  in
        rec 
finishing  with  (RepUR  ``genrec  so\_apply``  0  THEN  Auto)

---

Home Index