---

Step * of Lemma filter_is_nil

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

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[P:T  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[L:T  List].    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  ((RWO  "l\_all\_cons"  (-1)  THENM  AutoSplit)  THENA  Try  (Complete  (Auto)))
  THEN  BackThruSomeHyp
  THEN  Auto)

---

Home Index