---

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


1. A : Type
2. B : Type
3. bb : bag(A)
4. f : A ⟶ bag(B)
5. u : A
6. v : A List
7. bag-bind(v + bb;f) = (bag-bind(v;f) + bag-bind(bb;f)) ∈ bag(B)
⊢ ((f u) + bag-bind(v + bb;f)) = (((f u) + bag-bind(v;f)) + bag-bind(bb;f)) ∈ bag(B)
BY
{ (RWO "-1" 0 THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  bb  :  bag(A)
4.  f  :  A  {}\mrightarrow{}  bag(B)
5.  u  :  A
6.  v  :  A  List
7.  bag-bind(v  +  bb;f)  =  (bag-bind(v;f)  +  bag-bind(bb;f))
\mvdash{}  ((f  u)  +  bag-bind(v  +  bb;f))  =  (((f  u)  +  bag-bind(v;f))  +  bag-bind(bb;f))


By

---

Latex:
(RWO  "-1"  0  THEN  Auto)\mcdot{}

---

Home Index