---

Step * of Lemma mapc_wf

∀[A,B:Type]. ∀[f:A ⟶ B].  (mapc(f) ∈ (A List) ⟶ (B List))
BY
{ (UnivCD THENA Auto) }

1
1. A : Type
2. B : Type
3. f : A ⟶ B
⊢ mapc(f) ∈ (A List) ⟶ (B List)

---

Latex:

---

Latex:
\mforall{}[A,B:Type].  \mforall{}[f:A  {}\mrightarrow{}  B].    (mapc(f)  \mmember{}  (A  List)  {}\mrightarrow{}  (B  List))


By

---

Latex:
(UnivCD  THENA  Auto)

---

Home Index