Step * 1 of Lemma not_over_exists


1. Type
2. T ⟶ ℙ
3. ¬(∃x:T. Q[x])
4. T
⊢ ¬Q[x]
BY
(((D THENM 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