New theorems about finite maps and alists

Importing theorems that were useful in CakeML (https://cakeml.org).
Mostly by Ramana Kumar, some by Scott Owens.

Also removed the unnecessary ALL_DISTINCE assumption from
ALOOKUP_TABULATE.