---

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


1. A : Type
2. B : Type
3. bb : bag(A)
4. f : A ⟶ bag(B)
⊢ bag-bind(bb;f) = bag-bind(bb;f) ∈ bag(B)
BY
{ Auto }

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  bb  :  bag(A)
4.  f  :  A  {}\mrightarrow{}  bag(B)
\mvdash{}  bag-bind(bb;f)  =  bag-bind(bb;f)


By

---

Latex:
Auto

---

Home Index