---

Step * of Lemma not_squash

∀[p:ℙ]. uiff(¬↓p;¬p)
BY
{ Auto }

---

Latex:

---

Latex:
\mforall{}[p:\mBbbP{}].  uiff(\mneg{}\mdownarrow{}p;\mneg{}p)


By

---

Latex:
Auto

---

Home Index