---

Step * 2 of Lemma bag-combine-size


1. A : Type
2. B : Type
3. f : A ⟶ bag(B)
4. as : A List
5. bs : A List
6. permutation(A;as;bs)
⊢ #(⋃a∈as.f[a]) = #(⋃a∈bs.f[a]) ∈ ℕ
BY
{ TACTIC:(Subst ⌜as = bs ∈ bag(A)⌝ 0⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  f  :  A  {}\mrightarrow{}  bag(B)
4.  as  :  A  List
5.  bs  :  A  List
6.  permutation(A;as;bs)
\mvdash{}  \#(\mcup{}a\mmember{}as.f[a])  =  \#(\mcup{}a\mmember{}bs.f[a])


By

---

Latex:
TACTIC:(Subst  \mkleeneopen{}as  =  bs\mkleeneclose{}  0\mcdot{}  THEN  Auto)

---

Home Index