---

Step * 1 of Lemma mon_reduce_append


1. g : IMonoid
2. as : |g| List
3. bs : |g| List
⊢ (Π as @ bs) = ((Π as) * (Π bs)) ∈ |g|
BY
{ ((ListInd 2 THENM (AbReduce 0 THEN RW MonNormC 0)) THEN Auto) }

---

Latex:

---

Latex:

1.  g  :  IMonoid
2.  as  :  |g|  List
3.  bs  :  |g|  List
\mvdash{}  (\mPi{}  as  @  bs)  =  ((\mPi{}  as)  *  (\mPi{}  bs))


By

---

Latex:
((ListInd  2  THENM  (AbReduce  0  THEN  RW  MonNormC  0))  THEN  Auto)

---

Home Index