---

Step * 1 of Lemma mon_for_functionality_wrt_permr


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|
BY
{ (% Important for later that we use RevHypC rather than HypC %  Unfold `tlambda` 0 THEN RWH (RevHypC 7) 0 THEN Auto) }

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.f[x];as)) = (Π map(λx.f'[x];as)) ∈ |g|

---

Latex:

---

Latex:

1.  g  :  IAbMonoid
2.  A  :  Type
3.  as  :  A  List
4.  as'  :  A  List
5.  f  :  A  {}\mrightarrow{}  |g|
6.  f'  :  A  {}\mrightarrow{}  |g|
7.  as  \mequiv{}(A)  as'
8.  \mforall{}x:A.  (mem\_f(A;x;as)  {}\mRightarrow{}  (f[x]  =  f'[x]))
\mvdash{}  (\mPi{}  map(\mlambda{}x:A.  f[x];as))  =  (\mPi{}  map(\mlambda{}x:A.  f'[x];as'))


By

---

Latex:
(\%  Important  for  later  that  we  use  RevHypC  rather  than  HypC  \% 
  Unfold  `tlambda`  0
  THEN  RWH  (RevHypC  7)  0
  THEN  Auto)

---

Home Index