---

Step * 2 1 1 1 of Lemma map-as-map-upto


1. F : Top
2. u : Top
3. v : Top List
4. indxs : ℕ||v|| List
⊢ map(λi.F[v[i]];indxs) ~ map(λx.F[[u / v][x + 1]];indxs)
BY
{ (ListInd (-1) THEN Reduce 0 THEN EqCD THEN Try (Trivial)) }

1
1. F : Top
2. u : Top
3. v : Top List
4. u1 : ℕ||v||
5. v1 : ℕ||v|| List
6. map(λi.F[v[i]];v1) ~ map(λx.F[[u / v][x + 1]];v1)
⊢ F[v[u1]] ~ F[[u / v][u1 + 1]]

---

Latex:

---

Latex:

1.  F  :  Top
2.  u  :  Top
3.  v  :  Top  List
4.  indxs  :  \mBbbN{}||v||  List
\mvdash{}  map(\mlambda{}i.F[v[i]];indxs)  \msim{}  map(\mlambda{}x.F[[u  /  v][x  +  1]];indxs)


By

---

Latex:
(ListInd  (-1)  THEN  Reduce  0  THEN  EqCD  THEN  Try  (Trivial))

---

Home Index