---

Step * 1 of Lemma apply_alist-eager-map2


1. A : Type
2. L : A List
3. T : Type
4. value-type(T)
5. T ⊆r Base
6. eq : EqDecider(T)
7. g : A ⟶ T
8. f : Top
9. i : {i:T| (i ∈ eager-map(g;L))} 
10. apply_alist(eq;eager-map(λi.<i, f i>;eager-map(g;L));i) ~ f i
⊢ apply_alist(eq;eager-map(λa.<g a, f (g a)>;L);i) ~ apply_alist(eq;eager-map(λi.<i, f i>;eager-map(g;L));i)
BY
{ (EqCD THEN Try (Trivial)) }

1
1. A : Type
2. L : A List
3. T : Type
4. value-type(T)
5. T ⊆r Base
6. eq : EqDecider(T)
7. g : A ⟶ T
8. f : Top
9. i : {i:T| (i ∈ eager-map(g;L))} 
10. apply_alist(eq;eager-map(λi.<i, f i>;eager-map(g;L));i) ~ f i
⊢ eager-map(λa.<g a, f (g a)>;L) ~ eager-map(λi.<i, f i>;eager-map(g;L))

---

Latex:

---

Latex:

1.  A  :  Type
2.  L  :  A  List
3.  T  :  Type
4.  value-type(T)
5.  T  \msubseteq{}r  Base
6.  eq  :  EqDecider(T)
7.  g  :  A  {}\mrightarrow{}  T
8.  f  :  Top
9.  i  :  \{i:T|  (i  \mmember{}  eager-map(g;L))\} 
10.  apply\_alist(eq;eager-map(\mlambda{}i.<i,  f  i>eager-map(g;L));i)  \msim{}  f  i
\mvdash{}  apply\_alist(eq;eager-map(\mlambda{}a.<g  a,  f  (g  a)>L);i) 
\msim{}  apply\_alist(eq;eager-map(\mlambda{}i.<i,  f  i>eager-map(g;L));i)


By

---

Latex:
(EqCD  THEN  Try  (Trivial))

---

Home Index