---

Step * of Lemma member-filter

No Annotations
∀[T:Type]. ∀P:T ⟶ 𝔹. ∀L:T List. ∀x:{x:T| ↑P[x]} .  ((x ∈ filter(λx.P[x];L)) ⇐⇒ (x ∈ L))
BY
{ (InductionOnList THEN Reduce 0 THEN ((ParallelLast THEN AutoSplit) ORELSE Auto)) }

1
1. [T] : Type
2. P : T ⟶ 𝔹
3. u : T
4. v : T List
5. ∀x:{x:T| ↑P[x]} . ((x ∈ filter(λx.P[x];v)) ⇐⇒ (x ∈ v))
6. x : {x:T| ↑P[x]} 
7. (x ∈ filter(λx.P[x];v)) ⇐⇒ (x ∈ v)
8. ↑P[u]
⊢ (x ∈ [u / filter(λx.P[x];v)]) ⇐⇒ (x ∈ [u / v])

2
1. [T] : Type
2. P : T ⟶ 𝔹
3. u : T
4. ¬↑P[u]
5. v : T List
6. ∀x:{x:T| ↑P[x]} . ((x ∈ filter(λx.P[x];v)) ⇐⇒ (x ∈ v))
7. x : {x:T| ↑P[x]} 
8. (x ∈ filter(λx.P[x];v)) ⇐⇒ (x ∈ v)
⊢ (x ∈ filter(λx.P[x];v)) ⇐⇒ (x ∈ [u / v])

---

Latex:

---

Latex:
No  Annotations
\mforall{}[T:Type].  \mforall{}P:T  {}\mrightarrow{}  \mBbbB{}.  \mforall{}L:T  List.  \mforall{}x:\{x:T|  \muparrow{}P[x]\}  .    ((x  \mmember{}  filter(\mlambda{}x.P[x];L))  \mLeftarrow{}{}\mRightarrow{}  (x  \mmember{}  L))


By

---

Latex:
(InductionOnList  THEN  Reduce  0  THEN  ((ParallelLast  THEN  AutoSplit)  ORELSE  Auto))

---

Home Index