---

Step * 1 of Lemma hd_map


1. T : Type
2. T' : Type
3. a : T List+
4. f : T ⟶ T'
⊢ hd(map(f;a)) = (f hd(a)) ∈ T'
BY
{ (((D 3 THEN ListInd 3) THEN Reduce 0) THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  T'  :  Type
3.  a  :  T  List\msupplus{}
4.  f  :  T  {}\mrightarrow{}  T'
\mvdash{}  hd(map(f;a))  =  (f  hd(a))


By

---

Latex:
(((D  3  THEN  ListInd  3)  THEN  Reduce  0)  THEN  Auto)

---

Home Index