---

Step * of Lemma bag-bind-append2

∀[A,B:Type]. ∀[F,G:A ⟶ bag(B)]. ∀[ba:bag(A)].
  (bag-bind(ba;λa.((F a) + (G a))) = (bag-bind(ba;F) + bag-bind(ba;G)) ∈ bag(B))
BY
{ (Auto
   THEN D -1
   THEN Auto
   THEN RenameVar `as' 5
   THEN RenameVar `bs' 6
   THEN Subst ⌜bag-bind(as;λa.((F a) + (G a))) = (bag-bind(as;F) + bag-bind(as;G)) ∈ bag(B)⌝ 0⋅
   THEN Auto) }

1
.....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)

---

Latex:

---

Latex:
\mforall{}[A,B:Type].  \mforall{}[F,G:A  {}\mrightarrow{}  bag(B)].  \mforall{}[ba:bag(A)].
    (bag-bind(ba;\mlambda{}a.((F  a)  +  (G  a)))  =  (bag-bind(ba;F)  +  bag-bind(ba;G)))


By

---

Latex:
(Auto
  THEN  D  -1
  THEN  Auto
  THEN  RenameVar  `as'  5
  THEN  RenameVar  `bs'  6
  THEN  Subst  \mkleeneopen{}bag-bind(as;\mlambda{}a.((F  a)  +  (G  a)))  =  (bag-bind(as;F)  +  bag-bind(as;G))\mkleeneclose{}  0\mcdot{}
  THEN  Auto)

---

Home Index