---

Step * 2 of Lemma not_over_exists_uniform


1. T : Type
2. Q : T ⟶ ℙ
3. ∀[x:T]. (¬Q[x])
⊢ ¬(∃x:T. Q[x])
BY
{ (((D 0 THENM D (-1)) THENM With ⌜x⌝ (D 3)) THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  Q  :  T  {}\mrightarrow{}  \mBbbP{}
3.  \mforall{}[x:T].  (\mneg{}Q[x])
\mvdash{}  \mneg{}(\mexists{}x:T.  Q[x])


By

---

Latex:
(((D  0  THENM  D  (-1))  THENM  With  \mkleeneopen{}x\mkleeneclose{}  (D  3))  THEN  Auto)

---

Home Index