---

Step * of Lemma mon_for_functionality_wrt_permr

No Annotations
∀g:IAbMonoid. ∀A:Type. ∀as,as':A List. ∀f,f':A ⟶ |g|.
  ((as ≡(A) as')
  ⇒ (∀x:A. (mem_f(A;x;as) ⇒ (f[x] = f'[x] ∈ |g|)))
  ⇒ ((For{g} x ∈ as. f[x]) = (For{g} x ∈ as'. f'[x]) ∈ |g|))
BY
{ (((UnivCD THENA Auto) THEN RepUnfolds ``mon_for for`` 0) THEN Fold `mon_reduce` 0) }

1
1. g : IAbMonoid
2. A : Type
3. as : A List
4. as' : A List
5. f : A ⟶ |g|
6. f' : A ⟶ |g|
7. as ≡(A) as'
8. ∀x:A. (mem_f(A;x;as) ⇒ (f[x] = f'[x] ∈ |g|))
⊢ (Π map(λx:A. f[x];as)) = (Π map(λx:A. f'[x];as')) ∈ |g|

---

Latex:

---

Latex:
No  Annotations
\mforall{}g:IAbMonoid.  \mforall{}A:Type.  \mforall{}as,as':A  List.  \mforall{}f,f':A  {}\mrightarrow{}  |g|.
    ((as  \mequiv{}(A)  as')
    {}\mRightarrow{}  (\mforall{}x:A.  (mem\_f(A;x;as)  {}\mRightarrow{}  (f[x]  =  f'[x])))
    {}\mRightarrow{}  ((For\{g\}  x  \mmember{}  as.  f[x])  =  (For\{g\}  x  \mmember{}  as'.  f'[x])))


By

---

Latex:
(((UnivCD  THENA  Auto)  THEN  RepUnfolds  ``mon\_for  for``  0)  THEN  Fold  `mon\_reduce`  0)

---

Home Index