---

Step * 1 1 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
⊢ eager-map(λa.<g a, f (g a)>;L) ~ eager-map(λi.<i, f i>;eager-map(g;L))
BY
{ ((GenConcl ⌜f = F ∈ (T ⟶ Top)⌝⋅ THENA Auto)
   THEN ListInd 2
   THEN Reduce 0
   THEN Auto
   THEN RepeatFor 2 ((CallByValueReduce 0 THENA Auto))
   THEN Reduce 0
   THEN CallByValueReduce 0
   THEN Auto) }

---

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
\mvdash{}  eager-map(\mlambda{}a.<g  a,  f  (g  a)>L)  \msim{}  eager-map(\mlambda{}i.<i,  f  i>eager-map(g;L))


By

---

Latex:
((GenConcl  \mkleeneopen{}f  =  F\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  ListInd  2
  THEN  Reduce  0
  THEN  Auto
  THEN  RepeatFor  2  ((CallByValueReduce  0  THENA  Auto))
  THEN  Reduce  0
  THEN  CallByValueReduce  0
  THEN  Auto)

---

Home Index