---

Step * of Lemma map-as-map-upto

∀[F:Top]. ∀[L:Top List].  (map(λx.F[x];L) ~ map(λi.F[L[i]];upto(||L||)))
BY
{ (InductionOnList
   THEN Reduce 0
   THEN Try (Trivial)
   THEN RWO "-1" 0
   THEN Subst' upto(||v|| + 1) ~ [0 / map(λi.(i + 1);upto(||v||))] 0⋅) }

1
.....equality..... 
1. F : Top
2. u : Top
3. v : Top List
4. map(λx.F[x];v) ~ map(λi.F[v[i]];upto(||v||))
⊢ upto(||v|| + 1) ~ [0 / map(λi.(i + 1);upto(||v||))]

2
1. F : Top
2. u : Top
3. v : Top List
4. map(λx.F[x];v) ~ map(λi.F[v[i]];upto(||v||))
⊢ [F[u] / map(λi.F[v[i]];upto(||v||))] ~ map(λi.F[[u / v][i]];[0 / map(λi.(i + 1);upto(||v||))])

---

Latex:

---

Latex:
\mforall{}[F:Top].  \mforall{}[L:Top  List].    (map(\mlambda{}x.F[x];L)  \msim{}  map(\mlambda{}i.F[L[i]];upto(||L||)))


By

---

Latex:
(InductionOnList
  THEN  Reduce  0
  THEN  Try  (Trivial)
  THEN  RWO  "-1"  0
  THEN  Subst'  upto(||v||  +  1)  \msim{}  [0  /  map(\mlambda{}i.(i  +  1);upto(||v||))]  0\mcdot{})

---

Home Index