---

Step * of Lemma altneg-altneg

∀[T:Type]. ∀[X:n:ℕ ⟶ (ℕn ⟶ T) ⟶ 𝔹].  (¬(¬(X)) = X ∈ (n:ℕ ⟶ (ℕn ⟶ T) ⟶ 𝔹))
BY
{ (Auto THEN RepeatFor 2 ((FunExt THENA Auto)) THEN RepUR ``altneg`` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[X:n:\mBbbN{}  {}\mrightarrow{}  (\mBbbN{}n  {}\mrightarrow{}  T)  {}\mrightarrow{}  \mBbbB{}].    (\mneg{}(\mneg{}(X))  =  X)


By

---

Latex:
(Auto  THEN  RepeatFor  2  ((FunExt  THENA  Auto))  THEN  RepUR  ``altneg``  0  THEN  Auto)

---

Home Index