Def as @ bs == Case of as; nil  bs ; a.as'  cons(a; (as' @ bs))  (recursive)

is mentioned by

Thm* 'a,'b:S, f:('a'b), l1,l2:'a List. Thm* map(f;l1 @ l2) = (map(f;l1) @ map(f;l2))	[map_append_2]
Thm* 'a:S, l1,l2:'a List. ||l1 @ l2|| = ||l1||+||l2||	[length_append_2]
Thm* 'a:S, l1,l2,l3:'a List. (l1 @ (l2 @ l3)) = ((l1 @ l2) @ l3)	[append_assoc_2]

In prior sections: list 1 hol list 1

Try larger context: HOLlib IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html