list 3 jlc Sections Support(jlc) Doc

Def ||as|| == Case of as; nil 0 ; a.as' ||as'||+1 (recursive)

is mentioned by

Thm* eq:{T}, L:T List. ||L||1 hd(L)(eq) L[hd_is_member_lemma]

In prior sections: list 1


list 3 jlc Sections Support(jlc) Doc