---

Step * of Lemma not-not-l_all-xmiddle

No Annotations
∀[T:Type]. ∀[L:T List]. ∀[P:{x:T| (x ∈ L)}  ⟶ ℙ].  (¬¬(∀x∈L.P[x] ∨ (¬P[x])))
BY
{ (Auto
   THEN (InstLemma `not-not-all-int_seg-xmiddle` [⌜0⌝;⌜||L||⌝;⌜λ2i.P[L[i]]⌝]⋅ THENA Auto)
   THEN Unfold `l_all` 0
   THEN Trivial) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[T:Type].  \mforall{}[L:T  List].  \mforall{}[P:\{x:T|  (x  \mmember{}  L)\}    {}\mrightarrow{}  \mBbbP{}].    (\mneg{}\mneg{}(\mforall{}x\mmember{}L.P[x]  \mvee{}  (\mneg{}P[x])))


By

---

Latex:
(Auto
  THEN  (InstLemma  `not-not-all-int\_seg-xmiddle`  [\mkleeneopen{}0\mkleeneclose{};\mkleeneopen{}||L||\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}i.P[L[i]]\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  Unfold  `l\_all`  0
  THEN  Trivial)

---

Home Index