---

Step * 1 of Lemma filter_trivial


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

---

Latex:

---

Latex:

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


By

---

Latex:
((RWO  "l\_all\_cons"  (-2))  THEN  Auto)

---

Home Index