---

Step * of Lemma eager-map-append-sq

∀[T:Type]
  ∀[A:Type]. ∀[f:A ⟶ T]. ∀[as:A List]. ∀[bs:T List].  (eager-map-append(f;as;bs) ~ map(f;rev(as)) @ bs) 
  supposing value-type(T)
BY
{ (InductionOnList THEN Reduce 0) }

1
1. T : Type
2. value-type(T)
3. A : Type
4. f : A ⟶ T
⊢ ∀[bs:T List]. (bs ~ bs)

2
1. T : Type
2. value-type(T)
3. A : Type
4. f : A ⟶ T
5. u : A
6. v : A List
7. ∀[bs:T List]. (eager-map-append(f;v;bs) ~ map(f;rev(v)) @ bs)
⊢ ∀[bs:T List]. (eager-map-append(f;[u / v];bs) ~ map(f;rev([u / v])) @ bs)

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}[A:Type].  \mforall{}[f:A  {}\mrightarrow{}  T].  \mforall{}[as:A  List].  \mforall{}[bs:T  List].
        (eager-map-append(f;as;bs)  \msim{}  map(f;rev(as))  @  bs) 
    supposing  value-type(T)


By

---

Latex:
(InductionOnList  THEN  Reduce  0)

---

Home Index