---

Step * of Lemma apply_alist-eager-map2

∀[A:Type]. ∀[L:A List]. ∀[T:Type].
  ∀[eq:EqDecider(T)]. ∀[g:A ⟶ T]. ∀[f:Top]. ∀[i:{i:T| (i ∈ eager-map(g;L))} ].
    (apply_alist(eq;eager-map(λa.<g a, f (g a)>;L);i) ~ f i) 
  supposing value-type(T) ∧ (T ⊆r Base)
BY
{ (Auto
   THEN (InstLemma `apply_alist-eager-map` [⌜T⌝;⌜eq⌝;⌜f⌝;⌜eager-map(g;L)⌝;⌜i⌝]⋅ THENA Auto)
   THEN RevHypSubst' (-1) 0) }

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
⊢ 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)

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[L:A  List].  \mforall{}[T:Type].
    \mforall{}[eq:EqDecider(T)].  \mforall{}[g:A  {}\mrightarrow{}  T].  \mforall{}[f:Top].  \mforall{}[i:\{i:T|  (i  \mmember{}  eager-map(g;L))\}  ].
        (apply\_alist(eq;eager-map(\mlambda{}a.<g  a,  f  (g  a)>L);i)  \msim{}  f  i) 
    supposing  value-type(T)  \mwedge{}  (T  \msubseteq{}r  Base)


By

---

Latex:
(Auto
  THEN  (InstLemma  `apply\_alist-eager-map`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}eq\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}eager-map(g;L)\mkleeneclose{};\mkleeneopen{}i\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  RevHypSubst'  (-1)  0)

---

Home Index