Step
*
of Lemma
hd_wf_listp
∀[A:Type]. ∀[l:A List+].  (hd(l) ∈ A)
BY
{ Auto }
Latex:
Latex:
\mforall{}[A:Type].  \mforall{}[l:A  List\msupplus{}].    (hd(l)  \mmember{}  A)
By
Latex:
Auto
Home
Index