---

Step * 2 of Lemma filter_functionality


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 
BY
{ (FHyp 4 [-1] THEN Auto) }

---

Latex:

---

Latex:

1.  A  :  Type
2.  u  :  A
3.  v  :  A  List
4.  \mforall{}[f1,f2:A  {}\mrightarrow{}  \mBbbB{}].    filter(f1;v)  \msim{}  filter(f2;v)  supposing  f1  =  f2
5.  [f1]  :  A  {}\mrightarrow{}  \mBbbB{}
6.  [f2]  :  A  {}\mrightarrow{}  \mBbbB{}
7.  [\%1]  :  f1  =  f2
\mvdash{}  if  f1  u  then  [u  /  filter(f1;v)]  else  filter(f1;v)  fi    \msim{}  if  f2  u
then  [u  /  filter(f2;v)]
else  filter(f2;v)
fi 


By

---

Latex:
(FHyp  4  [-1]  THEN  Auto)

---

Home Index