Commit 2019-02-18 09:48 9a2c13ab

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.