---

Step * of Lemma sq_stable_from_decidable

∀[P:ℙ]. (Dec(P) ⇒ SqStable(P))
BY
{ ((UnivCD THENM Backchain   ``sq_stable__from_stable stable__from_decidable``) THEN Auto) }

---

Latex:

---

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


By

---

Latex:
((UnivCD  THENM  Backchain      ``sq\_stable\_\_from\_stable  stable\_\_from\_decidable``)  THEN  Auto)

---

Home Index