---

Step * of Lemma bag-append-ac

∀[T:Type]. ∀[as,bs,cs:bag(T)].  ((as + bs + cs) = (bs + as + cs) ∈ bag(T))
BY
{ UnivCD THENA Auto }

1
1. T : Type
2. as : bag(T)
3. bs : bag(T)
4. cs : bag(T)
⊢ (as + bs + cs) = (bs + as + cs) ∈ bag(T)

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[as,bs,cs:bag(T)].    ((as  +  bs  +  cs)  =  (bs  +  as  +  cs))


By

---

Latex:
UnivCD  THENA  Auto

---

Home Index