---

Step * 1 of Lemma not-l_exists


1. T : Type
2. L : T List@i
3. P : {x:T| (x ∈ L)}  ⟶ ℙ
4. ∀x:T. (¬((x ∈ L) ∧ P[x]))@i
5. x : T@i
6. (x ∈ L)@i
7. P[x]@i
⊢ False
BY
{ (InstHyp [⌜x⌝] 4⋅ THEN Auto THEN D (-1) THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  L  :  T  List@i
3.  P  :  \{x:T|  (x  \mmember{}  L)\}    {}\mrightarrow{}  \mBbbP{}
4.  \mforall{}x:T.  (\mneg{}((x  \mmember{}  L)  \mwedge{}  P[x]))@i
5.  x  :  T@i
6.  (x  \mmember{}  L)@i
7.  P[x]@i
\mvdash{}  False


By

---

Latex:
(InstHyp  [\mkleeneopen{}x\mkleeneclose{}]  4\mcdot{}  THEN  Auto  THEN  D  (-1)  THEN  Auto)

---

Home Index