mathlib3

9a2c13ab - feat(data/alist,data/finmap): always insert key-value pair (#722)

feat(data/alist,data/finmap): always insert key-value pair (#722) * Change {alist,finmap}.insert to always insert the key-value pair instead of doing nothing if the inserted key is found. This allows for useful theorems such as lookup_insert. * Add list.keys and used key membership instead of exists/forall. This makes proofs easier in some places. * Add a few other useful theorems such as lookup_eq_none, lookup_erase, lookup_erase_ne.