---

Step * of Lemma hd_map

∀[T,T':Type]. ∀[a:T List+]. ∀[f:T ⟶ T'].  (hd(map(f;a)) = (f hd(a)) ∈ T')
BY
{ (UnivCD THENA Auto) }

1
1. T : Type
2. T' : Type
3. a : T List+
4. f : T ⟶ T'
⊢ hd(map(f;a)) = (f hd(a)) ∈ T'

---

Latex:

---

Latex:
\mforall{}[T,T':Type].  \mforall{}[a:T  List\msupplus{}].  \mforall{}[f:T  {}\mrightarrow{}  T'].    (hd(map(f;a))  =  (f  hd(a)))


By

---

Latex:
(UnivCD  THENA  Auto)

---

Home Index