---

Step * of Lemma apply_alist-eager-map-atom

∀[T:Type]. ∀[L:T List]. ∀[g:T ⟶ Atom]. ∀[f:Top]. ∀[i:{i:Atom| (i ∈ eager-map(g;L))} ].
  (apply_alist(AtomDeq;eager-map(λa.<g a, f (g a)>;L);i) ~ f i)
BY
{ (Auto THEN BLemma `apply_alist-eager-map2` THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[L:T  List].  \mforall{}[g:T  {}\mrightarrow{}  Atom].  \mforall{}[f:Top].  \mforall{}[i:\{i:Atom|  (i  \mmember{}  eager-map(g;L))\}  ].
    (apply\_alist(AtomDeq;eager-map(\mlambda{}a.<g  a,  f  (g  a)>L);i)  \msim{}  f  i)


By

---

Latex:
(Auto  THEN  BLemma  `apply\_alist-eager-map2`  THEN  Auto)

---

Home Index