---

Step * 1 1 1 of Lemma bag-bind-filter


1. A : Type
2. B : Type
3. p : A ⟶ 𝔹
4. f : {a:A| ↑p[a]}  ⟶ bag(B)
⊢ [] = [] ∈ bag(B)
BY
{ (Fold `empty-bag` 0 THEN Auto) }

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  p  :  A  {}\mrightarrow{}  \mBbbB{}
4.  f  :  \{a:A|  \muparrow{}p[a]\}    {}\mrightarrow{}  bag(B)
\mvdash{}  []  =  []


By

---

Latex:
(Fold  `empty-bag`  0  THEN  Auto)

---

Home Index