---

Step * 2 of Lemma filter_trivial


1. T : Type
2. P : T ⟶ 𝔹
3. u : T
4. ¬↑(P u)
5. v : T List
6. filter(P;v) ~ v supposing (∀x∈v.↑P[x])
7. (∀x∈[u / v].↑P[x])
⊢ filter(P;v) ~ [u / v]
BY
{ (D 4 THEN (RWO "l_all_cons" (-1)) THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  P  :  T  {}\mrightarrow{}  \mBbbB{}
3.  u  :  T
4.  \mneg{}\muparrow{}(P  u)
5.  v  :  T  List
6.  filter(P;v)  \msim{}  v  supposing  (\mforall{}x\mmember{}v.\muparrow{}P[x])
7.  (\mforall{}x\mmember{}[u  /  v].\muparrow{}P[x])
\mvdash{}  filter(P;v)  \msim{}  [u  /  v]


By

---

Latex:
(D  4  THEN  (RWO  "l\_all\_cons"  (-1))  THEN  Auto)

---

Home Index