---

Step * 1 of Lemma not-l_all-dec


1. [T] : Type
2. L : T List@i
3. P : T ⟶ ℙ@i'
4. ∀x:T. Dec(P[x])@i
5. ¬(∀x∈L.P[x])@i
⊢ (∃x∈L. ¬P[x])
BY
{ ((Decide ⌜(∃x∈L. ¬P[x])⌝⋅ THEN Auto)
   THEN (RWO "not-l_exists" (-1) THEN Auto)
   THEN D (-2)
   THEN (All(RWO "l_all_iff") THEN Auto)
   THEN InstHyp [⌜x⌝] (-3)⋅
   THEN Auto
   THEN Decide ⌜P[x]⌝⋅
   THEN Auto) }

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  L  :  T  List@i
3.  P  :  T  {}\mrightarrow{}  \mBbbP{}@i'
4.  \mforall{}x:T.  Dec(P[x])@i
5.  \mneg{}(\mforall{}x\mmember{}L.P[x])@i
\mvdash{}  (\mexists{}x\mmember{}L.  \mneg{}P[x])


By

---

Latex:
((Decide  \mkleeneopen{}(\mexists{}x\mmember{}L.  \mneg{}P[x])\mkleeneclose{}\mcdot{}  THEN  Auto)
  THEN  (RWO  "not-l\_exists"  (-1)  THEN  Auto)
  THEN  D  (-2)
  THEN  (All(RWO  "l\_all\_iff")  THEN  Auto)
  THEN  InstHyp  [\mkleeneopen{}x\mkleeneclose{}]  (-3)\mcdot{}
  THEN  Auto
  THEN  Decide  \mkleeneopen{}P[x]\mkleeneclose{}\mcdot{}
  THEN  Auto)

---

Home Index