---

Step * 1 of Lemma filter_is_nil3

.....assertion..... 
∀[T:Type]. ∀[L:T List]. ∀[P:T ⟶ 𝔹].  filter(P;L) ~ [] supposing (∀x∈L.¬↑P[x])
BY
{ (InductionOnList
   THEN Reduce 0
   THEN UnivCD
   THEN Try (Complete ((Auto THEN D -1 THEN Auto)))
   THEN (RWO "l_all_cons" (-1) THENA Auto)
   THEN AutoSplit
   THEN BackThruSomeHyp
   THEN Auto)⋅ }

---

Latex:

---

Latex:
.....assertion..... 
\mforall{}[T:Type].  \mforall{}[L:T  List].  \mforall{}[P:T  {}\mrightarrow{}  \mBbbB{}].    filter(P;L)  \msim{}  []  supposing  (\mforall{}x\mmember{}L.\mneg{}\muparrow{}P[x])


By

---

Latex:
(InductionOnList
  THEN  Reduce  0
  THEN  UnivCD
  THEN  Try  (Complete  ((Auto  THEN  D  -1  THEN  Auto)))
  THEN  (RWO  "l\_all\_cons"  (-1)  THENA  Auto)
  THEN  AutoSplit
  THEN  BackThruSomeHyp
  THEN  Auto)\mcdot{}

---

Home Index