---

Step * of Lemma null-filter2

∀[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 SplitOnHypITE -1 
   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  SplitOnHypITE  -1 
  THEN  Auto)

---

Home Index