---

Step * of Lemma uniform-TI-less

∀[P:ℕ ⟶ ℙ]. uniform-TI(ℕ;x,y.y < x;x.P[x])
BY
{ (InstLemma `uniform-comp-nat-induction` [] THEN RepUR ``uniform-TI`` 0 THEN RepeatFor 5 (ParallelLast)) }

---

Latex:

---

Latex:
\mforall{}[P:\mBbbN{}  {}\mrightarrow{}  \mBbbP{}].  uniform-TI(\mBbbN{};x,y.y  <  x;x.P[x])


By

---

Latex:
(InstLemma  `uniform-comp-nat-induction`  []
  THEN  RepUR  ``uniform-TI``  0
  THEN  RepeatFor  5  (ParallelLast))

---

Home Index