---

Step * of Lemma map_append

∀[A,B:Type]. ∀[f:A ⟶ B]. ∀[as,as':A List].  (map(f;as @ as') = (map(f;as) @ map(f;as')) ∈ (B List))
BY
{ (RWO "map_append_sq" 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A,B:Type].  \mforall{}[f:A  {}\mrightarrow{}  B].  \mforall{}[as,as':A  List].    (map(f;as  @  as')  =  (map(f;as)  @  map(f;as')))


By

---

Latex:
(RWO  "map\_append\_sq"  0  THEN  Auto)

---

Home Index