---

Step * of Lemma dneg_elim

∀[A:ℙ]. (Dec(A) ⇒ A supposing ¬¬A)
BY
{ (Fold `stable` 0 THEN Lemma `stable__from_decidable`) }

---

Latex:

---

Latex:
\mforall{}[A:\mBbbP{}].  (Dec(A)  {}\mRightarrow{}  A  supposing  \mneg{}\mneg{}A)


By

---

Latex:
(Fold  `stable`  0  THEN  Lemma  `stable\_\_from\_decidable`)

---

Home Index