---

Step * of Lemma filter_functionality

∀[A:Type]. ∀[L:A List]. ∀[f1,f2:A ⟶ 𝔹].  filter(f1;L) ~ filter(f2;L) supposing f1 = f2 ∈ (A ⟶ 𝔹)
BY
{ ((InductionOnList THENA Auto) THEN Intros THEN Reduce 0) }

1
1. A : Type
2. [f1] : A ⟶ 𝔹
3. [f2] : A ⟶ 𝔹
4. [%] : f1 = f2 ∈ (A ⟶ 𝔹)
⊢ [] ~ []

2
1. A : Type
2. u : A
3. v : A List
4. ∀[f1,f2:A ⟶ 𝔹].  filter(f1;v) ~ filter(f2;v) supposing f1 = f2 ∈ (A ⟶ 𝔹)
5. [f1] : A ⟶ 𝔹
6. [f2] : A ⟶ 𝔹
7. [%1] : f1 = f2 ∈ (A ⟶ 𝔹)
⊢ if f1 u then [u / filter(f1;v)] else filter(f1;v) fi  ~ if f2 u then [u / filter(f2;v)] else filter(f2;v) fi 

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[L:A  List].  \mforall{}[f1,f2:A  {}\mrightarrow{}  \mBbbB{}].    filter(f1;L)  \msim{}  filter(f2;L)  supposing  f1  =  f2


By

---

Latex:
((InductionOnList  THENA  Auto)  THEN  Intros  THEN  Reduce  0)

---

Home Index