---

Step * of Lemma bnot_thru_exists

∀A:Type. ∀as:A List. ∀f:A ⟶ 𝔹.  ¬b(∃bx(:A) ∈ as. f[x]) = ∀bx(:A) ∈ as. (¬bf[x])
BY
{ (InductionOnListA THEN Reduce 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}A:Type.  \mforall{}as:A  List.  \mforall{}f:A  {}\mrightarrow{}  \mBbbB{}.    \mneg{}\msubb{}(\mexists{}\msubb{}x(:A)  \mmember{}  as.  f[x])  =  \mforall{}\msubb{}x(:A)  \mmember{}  as.  (\mneg{}\msubb{}f[x])


By

---

Latex:
(InductionOnListA  THEN  Reduce  0  THEN  Auto)

---

Home Index