---

Step * of Lemma null-filter

∀[T:Type]. ∀[P:T ⟶ 𝔹]. ∀[L:T List].  uiff(↑null(filter(P;L));(∀x∈L.¬↑P[x]))
BY
{ (((UnivCD THENA Auto) THEN (RepeatFor 2 (D 0) THENA Auto))
   THEN Try ((BLemma `null_filter` THEN Auto))
   THEN ListInd (-2)
   THEN Reduce 0
   THEN Auto
   THEN Try ((BLemma `l_all_nil` THEN Auto))
   THEN BLemma `l_all_cons` 
   THEN Auto
   THEN Try ((SplitOnHypITE (-1) THEN Auto THEN Reduce (-2) THEN Auto))
   THEN SplitOnHypITE (-2)
   THEN Auto
   THEN RepUR ``so_apply`` (-2)
   THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(((UnivCD  THENA  Auto)  THEN  (RepeatFor  2  (D  0)  THENA  Auto))
  THEN  Try  ((BLemma  `null\_filter`  THEN  Auto))
  THEN  ListInd  (-2)
  THEN  Reduce  0
  THEN  Auto
  THEN  Try  ((BLemma  `l\_all\_nil`  THEN  Auto))
  THEN  BLemma  `l\_all\_cons` 
  THEN  Auto
  THEN  Try  ((SplitOnHypITE  (-1)  THEN  Auto  THEN  Reduce  (-2)  THEN  Auto))
  THEN  SplitOnHypITE  (-2)
  THEN  Auto
  THEN  RepUR  ``so\_apply``  (-2)
  THEN  Auto)

---

Home Index