---

Step * 1 of Lemma mon_for_append


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|
BY
{ (RWO "-2" 0 THEN Auto) }

---

Latex:

---

Latex:

1.  g  :  IMonoid
2.  A  :  Type
3.  f  :  A  {}\mrightarrow{}  |g|
4.  a  :  A
5.  as  :  A  List
6.  \mforall{}as':A  List
          ((For\{A,*,e\}  x  \mmember{}  as  @  as'.  f[x])  =  ((For\{A,*,e\}  x  \mmember{}  as.  f[x])  *  (For\{A,*,e\}  x  \mmember{}  as'.  f[x])))
7.  as'  :  A  List
\mvdash{}  (*  f[a]  (For\{A,*,e\}  x  \mmember{}  as  @  as'.  f[x]))
=  ((*  f[a]  (For\{A,*,e\}  x  \mmember{}  as.  f[x]))  *  (For\{A,*,e\}  x  \mmember{}  as'.  f[x]))


By

---

Latex:
(RWO  "-2"  0  THEN  Auto)

---

Home Index