---

Step * of Lemma exists-unit

∀P:Unit ⟶ ℙ. (∃x:Unit. P[x] ⇐⇒ P[⋅])
BY
{ (Auto THEN Auto THEN ExRepD THEN D 2⋅ THEN Fold `it` (-1) THEN Auto) }

---

Latex:

---

Latex:
\mforall{}P:Unit  {}\mrightarrow{}  \mBbbP{}.  (\mexists{}x:Unit.  P[x]  \mLeftarrow{}{}\mRightarrow{}  P[\mcdot{}])


By

---

Latex:
(Auto  THEN  Auto  THEN  ExRepD  THEN  D  2\mcdot{}  THEN  Fold  `it`  (-1)  THEN  Auto)

---

Home Index