---

Step * of Lemma bag-product-append

∀[as,bs,cs:Top List].  (as + bs × cs ~ as × cs + bs × cs)
BY
{ (Auto THEN ListInd 1 THEN Try ((Fold `empty-bag` 0 THEN (RWW "bag-product-empty" 0 THENM Reduce 0) THEN Auto))) }

1
1. bs : Top List
2. cs : Top List
3. u : Top
4. v : Top List
5. v + bs × cs ~ v × cs + bs × cs
⊢ [u / v] + bs × cs ~ [u / v] × cs + bs × cs

---

Latex:

---

Latex:
\mforall{}[as,bs,cs:Top  List].    (as  +  bs  \mtimes{}  cs  \msim{}  as  \mtimes{}  cs  +  bs  \mtimes{}  cs)


By

---

Latex:
(Auto
  THEN  ListInd  1
  THEN  Try  ((Fold  `empty-bag`  0  THEN  (RWW  "bag-product-empty"  0  THENM  Reduce  0)  THEN  Auto)))

---

Home Index