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