---

Step * of Lemma mon_for_append

No Annotations
∀g:IMonoid. ∀A:Type. ∀f:A ⟶ |g|. ∀as,as':A List.
  ((For{g} x ∈ as @ as'. f[x]) = ((For{g} x ∈ as. f[x]) * (For{g} x ∈ as'. f[x])) ∈ |g|)
BY
{ (Unfold `mon_for` 0 THEN InductionOnListA THEN Reduce 0 THEN Auto) }

1
1. g : IMonoid
2. A : Type
3. f : A ⟶ |g|
4. a : A
5. as : A List
6. ∀as':A List. ((For{A,*,e} x ∈ as @ as'. f[x]) = ((For{A,*,e} x ∈ as. f[x]) * (For{A,*,e} x ∈ as'. f[x])) ∈ |g|)
7. as' : A List
⊢ (* f[a] (For{A,*,e} x ∈ as @ as'. f[x])) = ((* f[a] (For{A,*,e} x ∈ as. f[x])) * (For{A,*,e} x ∈ as'. f[x])) ∈ |g|

---

Latex:

---

Latex:
No  Annotations
\mforall{}g:IMonoid.  \mforall{}A:Type.  \mforall{}f:A  {}\mrightarrow{}  |g|.  \mforall{}as,as':A  List.
    ((For\{g\}  x  \mmember{}  as  @  as'.  f[x])  =  ((For\{g\}  x  \mmember{}  as.  f[x])  *  (For\{g\}  x  \mmember{}  as'.  f[x])))


By

---

Latex:
(Unfold  `mon\_for`  0  THEN  InductionOnListA  THEN  Reduce  0  THEN  Auto)

---

Home Index