---

Step * of Lemma comb_for_hd_wf_listp

λA,l,z. hd(l) ∈ A:Type ⟶ l:A List+ ⟶ (↓True) ⟶ A
BY
{ (ProveOpCombinatorTyping Auto) `hd_wf_listp` }

---

Latex:

---

Latex:
\mlambda{}A,l,z.  hd(l)  \mmember{}  A:Type  {}\mrightarrow{}  l:A  List\msupplus{}  {}\mrightarrow{}  (\mdownarrow{}True)  {}\mrightarrow{}  A


By

---

Latex:
(ProveOpCombinatorTyping  Auto)  `hd\_wf\_listp`

---

Home Index