---

Step * 2 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
{ ((D 0 THENA Auto)
   THEN (All(RWO "l_all_iff") THENA Auto)
   THEN (All(RWO "l_exists_iff") THENA Auto)
   THEN ExRepD
   THEN InstHyp [⌜x⌝] (-1)⋅
   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.  (\mexists{}x\mmember{}L.  \mneg{}P[x])@i
\mvdash{}  \mneg{}(\mforall{}x\mmember{}L.P[x])


By

---

Latex:
((D  0  THENA  Auto)
  THEN  (All(RWO  "l\_all\_iff")  THENA  Auto)
  THEN  (All(RWO  "l\_exists\_iff")  THENA  Auto)
  THEN  ExRepD
  THEN  InstHyp  [\mkleeneopen{}x\mkleeneclose{}]  (-1)\mcdot{}
  THEN  Auto)

---

Home Index