---

Step * of Lemma uall-unit

∀P:Unit ⟶ ℙ. (∀[x:Unit]. P[x] ⇐⇒ P[⋅])
BY
{ (Auto THEN (Subst ⌜x ~ ⋅⌝ 0⋅ THEN 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  (Subst  \mkleeneopen{}x  \msim{}  \mcdot{}\mkleeneclose{}  0\mcdot{}  THEN  Auto)  THEN  (D  (-1)  THEN  Fold  `it`  0)  THEN  Auto)

---

Home Index