---

Step * of Lemma rec-case-map-sq

∀[f:Top]. ∀[l:Top List].  (rec-case(l) of [] => [] | a::as => r.[f[a] / r] ~ map(λa.f[a];l))
BY
{ (InductionOnList THEN Reduce 0 THEN EqCD THEN Trivial) }

---

Latex:

---

Latex:
\mforall{}[f:Top].  \mforall{}[l:Top  List].    (rec-case(l)  of  []  =>  []  |  a::as  =>  r.[f[a]  /  r]  \msim{}  map(\mlambda{}a.f[a];l))


By

---

Latex:
(InductionOnList  THEN  Reduce  0  THEN  EqCD  THEN  Trivial)

---

Home Index