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

Note that Lean's documentation is often inconsistent with its naming: e.g. a function called concat is said to append, a function called append is said to perform concatenation.

Comparison across languages

(m) means "mutates in place"

Language	Type	x :: xs	xs ++ [x]	xs ++ ys	xss[0] ++ xss[1] ++ ...
Lean	List	cons x xs	concat xs x	append xs ys	join xss
Lean	Fin n -> X	cons x xs	snoc xs x	append xs ys	We don't seem to have this. See below.*
Python	list	xs.insert(0, x) (m)	xs.append(x) (m)	operator.concat(xs, ys) (though append and extend also work)
Python	deque	xs.appendleft(x) (m)	xs.appendright(x) (m)	operator.concat(xs, ys)
PHP	Array	array_unshift()	array_push()	array_merge($xs, $ys)	array_merge(...$xss)
Cryptol	Sequence (size-dependent)	[x] # xs	xs # [x]	(#) (doc: "append").	join xss
Haskell	List	(:)	snoc	(++) (doc: "append")	concat
Scala	List	(::) or, more generically, (+:)	(:+)	(++) or (:::) or List.concat	List.flatten
Scala	Array	(+:), or (+:=) for (m)	(:+), or (:+=) for (m)	(++) or Array.concat	Array.flatten
Rust	Vec<n>	Vec::insert, with argument index as 0	Vec::push, docs describe as append.	Vec::append	Vec::concat

*

(Equiv.curry _ _ _).symm.trans ((finProdFinEquiv).arrowCongr (Equiv.refl _))