---

Step * of Lemma apply_alist-eager-map

∀[T:Type]
  ∀[eq:EqDecider(T)]. ∀[f:Top]. ∀[L:T List]. ∀[i:{i:T| (i ∈ L)} ].  (apply_alist(eq;eager-map(λi.<i, f i>;L);i) ~ f i) 
  supposing value-type(T) ∧ (T ⊆r Base)
BY
{ (InductionOnList
   THEN Auto
   THEN Reduce 0
   THEN (Assert f ∈ T ⟶ Top BY
               Auto)
   THEN (CallByValueReduce 0 THENA Auto)
   THEN Unfold `apply_alist` 0
   THEN Reduce 0
   THEN (InstLemma `deq_property` [⌜T⌝;⌜eq⌝;⌜u⌝;⌜i⌝]⋅ THENA Auto)
   THEN MoveToConcl (-1)
   THEN (GenConclTerm ⌜eq u i⌝⋅ THENA Auto)
   THEN Thin (-1)
   THEN D -1
   THEN Reduce 0
   THEN RepUR ``assert`` 0
   THEN Auto
   THEN BackThruSomeHyp
   THEN DVar `i'
   THEN OnMaybeHyp 10 (\h. (GenListD h THEN D h THEN Complete (Auto)))) }

---

Latex:

---

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


By

---

Latex:
(InductionOnList
  THEN  Auto
  THEN  Reduce  0
  THEN  (Assert  f  \mmember{}  T  {}\mrightarrow{}  Top  BY
                          Auto)
  THEN  (CallByValueReduce  0  THENA  Auto)
  THEN  Unfold  `apply\_alist`  0
  THEN  Reduce  0
  THEN  (InstLemma  `deq\_property`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}eq\mkleeneclose{};\mkleeneopen{}u\mkleeneclose{};\mkleeneopen{}i\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  MoveToConcl  (-1)
  THEN  (GenConclTerm  \mkleeneopen{}eq  u  i\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Thin  (-1)
  THEN  D  -1
  THEN  Reduce  0
  THEN  RepUR  ``assert``  0
  THEN  Auto
  THEN  BackThruSomeHyp
  THEN  DVar  `i'
  THEN  OnMaybeHyp  10  (\mbackslash{}h.  (GenListD  h  THEN  D  h  THEN  Complete  (Auto))))

---

Home Index