---

Step * of Lemma map-sq-mklist

∀[L:Top List]. ∀[f:Top].  (map(f;L) ~ mklist(||L||;λi.(f L[i])))
BY
{ (xxxInductionOnListxxx THEN Reduce 0 THEN Auto THEN (RWO "mklist-add1-cons" 0 THENA Auto) THEN Reduce 0 THEN EqCD) }

1
1. u : Top
2. v : Top List
3. ∀[f:Top]. (map(f;v) ~ mklist(||v||;λi.(f v[i])))
4. f : Top
⊢ f u ~ f u

2
1. u : Top
2. v : Top List
3. ∀[f:Top]. (map(f;v) ~ mklist(||v||;λi.(f v[i])))
4. f : Top
⊢ map(f;v) ~ mklist(||v||;λi.(f [u / v][i + 1]))

---

Latex:

---

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


By

---

Latex:
(xxxInductionOnListxxx
  THEN  Reduce  0
  THEN  Auto
  THEN  (RWO  "mklist-add1-cons"  0  THENA  Auto)
  THEN  Reduce  0
  THEN  EqCD)

---

Home Index