---

Step * 1 of Lemma not_over_exists_uniform


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

---

Latex:

---

Latex:

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


By

---

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

---

Home Index