(11steps) PrintForm Definitions list 3 jlc Sections Support(jlc) Doc

At: hd is member lemma

T:Type, eq:{T}, L:T List. ||L||1 hd(L)(eq) L
By: UnivCD
Generated subgoal:

11. T: Type
2. eq: {T}
3. L: T List
4. ||L||1
hd(L)(eq) L

About:
listassertnatural_numberuniverseimpliesall

(11steps) PrintForm Definitions list 3 jlc Sections Support(jlc) Doc