---

Step * 2 of Lemma bag-bind-append


1. A : Type
2. B : Type
3. as : Base
4. bs : Base
5. as = bs ∈ pertype(λas,bs. ((as ∈ A List) ∧ (bs ∈ A List) ∧ permutation(A;as;bs)))
6. as ∈ A List
7. bs ∈ A List
8. permutation(A;as;bs)
9. bb : bag(A)
10. f : A ⟶ bag(B)
⊢ (bag-bind(as;f) + bag-bind(bb;f)) = (bag-bind(bs;f) + bag-bind(bb;f)) ∈ bag(B)
BY
{ (Assert ⌜as = bs ∈ bag(A)⌝⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  as  :  Base
4.  bs  :  Base
5.  as  =  bs
6.  as  \mmember{}  A  List
7.  bs  \mmember{}  A  List
8.  permutation(A;as;bs)
9.  bb  :  bag(A)
10.  f  :  A  {}\mrightarrow{}  bag(B)
\mvdash{}  (bag-bind(as;f)  +  bag-bind(bb;f))  =  (bag-bind(bs;f)  +  bag-bind(bb;f))


By

---

Latex:
(Assert  \mkleeneopen{}as  =  bs\mkleeneclose{}\mcdot{}  THEN  Auto)

---

Home Index