---

Step * 1 of Lemma bag-bind-append

.....equality..... 
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 + bb;f) = (bag-bind(as;f) + bag-bind(bb;f)) ∈ bag(B)
BY
{ (ThinVar `bs' THEN (GenConclTerm ⌜as⌝⋅ THENA Auto) THEN ThinVar `as' THEN RenameVar `as' (-1)) }

1
1. A : Type
2. B : Type
3. bb : bag(A)
4. f : A ⟶ bag(B)
5. as : A List
⊢ bag-bind(as + bb;f) = (bag-bind(as;f) + bag-bind(bb;f)) ∈ bag(B)

---

Latex:

---

Latex:
.....equality..... 
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  +  bb;f)  =  (bag-bind(as;f)  +  bag-bind(bb;f))


By

---

Latex:
(ThinVar  `bs'  THEN  (GenConclTerm  \mkleeneopen{}as\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  ThinVar  `as'  THEN  RenameVar  `as'  (-1))

---

Home Index