---

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


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]]
BY
{ (RWO "select_cons_tl_sq" 0 THEN Auto) }

---

Latex:

---

Latex:

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


By

---

Latex:
(RWO  "select\_cons\_tl\_sq"  0  THEN  Auto)

---

Home Index