---

Step * of Lemma rev-map-append_wf

∀[A,B:Type].  ∀[f:A ⟶ B]. ∀[as:A List]. ∀[bs:B List].  (rev-map-append(f;as;bs) ∈ B List) supposing value-type(B)
BY
{ (InductionOnList THEN Auto THEN RecUnfold `rev-map-append` 0 THEN Reduce 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A,B:Type].
    \mforall{}[f:A  {}\mrightarrow{}  B].  \mforall{}[as:A  List].  \mforall{}[bs:B  List].    (rev-map-append(f;as;bs)  \mmember{}  B  List) 
    supposing  value-type(B)


By

---

Latex:
(InductionOnList  THEN  Auto  THEN  RecUnfold  `rev-map-append`  0  THEN  Reduce  0  THEN  Auto)

---

Home Index