---

Step * of Lemma squash_squash

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

---

Latex:

---

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


By

---

Latex:
Auto

---

Home Index