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