---

Step * 1 of Lemma filter_functionality


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

---

Latex:

---

Latex:

1.  A  :  Type
2.  [f1]  :  A  {}\mrightarrow{}  \mBbbB{}
3.  [f2]  :  A  {}\mrightarrow{}  \mBbbB{}
4.  [\%]  :  f1  =  f2
\mvdash{}  []  \msim{}  []


By

---

Latex:
Auto

---

Home Index