---

Step * of Lemma sq_stable__ex_nat_plus

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

---

Latex:

---

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


By

---

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

---

Home Index