---

Step * of Lemma sq_stable__ex_nat

∀[P:ℕ ⟶ ℙ]. ((∀m:ℕ. Dec(P[m])) ⇒ SqStable(∃m:ℕ. P[m]))
BY
{ ((InstLemma `sq_stable__ex_int_upper` [⌜0⌝]⋅ THENA Auto) THEN RepeatFor 6 (ParallelLast)) }

---

Latex:

---

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


By

---

Latex:
((InstLemma  `sq\_stable\_\_ex\_int\_upper`  [\mkleeneopen{}0\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  RepeatFor  6  (ParallelLast))

---

Home Index