---

Step * of Lemma all-unit

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

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  (D  (-1)  THEN  Fold  `it`  0)  THEN  Auto)

---

Home Index