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

At: hd is member lemma 1 1
1. T: Type
2. eq: {T}
3. L: T List

||nil||1 hd(nil)(eq) nil
By: Rewrite (HigherC length_unrollC) 0
Generated subgoals:

None

About:
listnilassertnatural_numberuniverseimplies

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