Alternate names for `List.concat` and `List.append`

This follows on from ideas in:

• https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/List.2Econcat.20and.20List.2Eappend/near/405811812
• https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/append.20and.20concat/near/299602232

Comparison across languages

(m) means "mutates in place"

Language	Type	x :: xs	xs ++ [x]	xs ++ ys	[xs] -> xss
Lean	List	cons x xs	concat xs x	append xs ys
Lean	Fin n -> X	cons x xs	snoc xs x	append xs ys
Python	list	xs.insert(0, x) (m)	xs.append(x) (m)	operator.concat(xs, ys)
Python	deque	xs.appendleft(x) (m)	xs.appendright(x) (m)	operator.concat(xs, ys)
PHP	Array	array_unshift()	array_push()	array_merge()
Cryptol	Sequence (size-dependent)	[x] # xs	xs # [x]	(#), called "append" in documentation.