---

Step * of Lemma sq_stable__from_stable

∀[P:ℙ]. (Stable{P} ⇒ SqStable(P))
BY
{ ((Unfolds ``sq_stable stable`` 0 THEN UnivCD) THENA Auto) }

1
1. [P] : ℙ
2. P supposing ¬¬P
3. ↓P
⊢ P

---

Latex:

---

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


By

---

Latex:
((Unfolds  ``sq\_stable  stable``  0  THEN  UnivCD)  THENA  Auto)

---

Home Index