---

Step * of Lemma mapl_wf

∀[A,B:Type]. ∀[L:A List]. ∀[f:{a:A| (a ∈ L)}  ⟶ B].  (mapl(f;L) ∈ B List)
BY
{ (Unfold `mapl` 0 THEN (InstLemma `map-wf2` []) THEN Trivial) }

---

Latex:

---

Latex:
\mforall{}[A,B:Type].  \mforall{}[L:A  List].  \mforall{}[f:\{a:A|  (a  \mmember{}  L)\}    {}\mrightarrow{}  B].    (mapl(f;L)  \mmember{}  B  List)


By

---

Latex:
(Unfold  `mapl`  0  THEN  (InstLemma  `map-wf2`  [])  THEN  Trivial)

---

Home Index