---

Step * 1 of Lemma bag-product-append


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
BY
{ ((RepUR ``bag-product bag-append`` 0 THEN Fold `bag-append` 0 THEN Fold `bag-product` 0)
   THEN HypSubst' (-1) 0
   THEN Unfold `bag-append` 0
   THEN RWO "append_assoc_sq" 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  bs  :  Top  List
2.  cs  :  Top  List
3.  u  :  Top
4.  v  :  Top  List
5.  v  +  bs  \mtimes{}  cs  \msim{}  v  \mtimes{}  cs  +  bs  \mtimes{}  cs
\mvdash{}  [u  /  v]  +  bs  \mtimes{}  cs  \msim{}  [u  /  v]  \mtimes{}  cs  +  bs  \mtimes{}  cs


By

---

Latex:
((RepUR  ``bag-product  bag-append``  0  THEN  Fold  `bag-append`  0  THEN  Fold  `bag-product`  0)
  THEN  HypSubst'  (-1)  0
  THEN  Unfold  `bag-append`  0
  THEN  RWO  "append\_assoc\_sq"  0
  THEN  Auto)

---

Home Index