---

Step * 1 of Lemma bag-bind-append2

.....equality..... 
1. A : Type
2. B : Type
3. F : A ⟶ bag(B)
4. G : A ⟶ bag(B)
5. as : Base
6. bs : Base
7. as = bs ∈ pertype(λas,bs. ((as ∈ A List) ∧ (bs ∈ A List) ∧ permutation(A;as;bs)))
8. as ∈ A List
9. bs ∈ A List
10. permutation(A;as;bs)
⊢ bag-bind(as;λa.((F a) + (G a))) = (bag-bind(as;F) + bag-bind(as;G)) ∈ bag(B)
BY
{ TACTIC:(ThinVar `bs' THEN (GenConclTerm ⌜as⌝⋅ THENA Auto) THEN ThinVar `as' THEN RenameVar `as' (-1)) }

1
1. A : Type
2. B : Type
3. F : A ⟶ bag(B)
4. G : A ⟶ bag(B)
5. as : A List@i
⊢ bag-bind(as;λa.((F a) + (G a))) = (bag-bind(as;F) + bag-bind(as;G)) ∈ bag(B)

---

Latex:

---

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


By

---

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

---

Home Index