Fix inconsistencies in `lookup` and `elem_of` lemmas for `list`
- Rename lemmas
elem_of_list_Xintolist_elem_of_Xto be consistent with thelist_lookup_Xlemmas. Some lemmas contained other inconsistencies (e.g.,_1and_2swapped), see CHANGELOG for details. - Change the order of the conjunction in
list_lookup_fmap_Some. The new version is(f <$> l) !! i = Some y ↔ ∃ x, y = f x ∧ l !! i = Some x, which makes it consistent withlist_elem_of_fmapand the corresponding lemmas for sets and maps. To be continued in other MR, insert link - Rename
list_alter_fmap→list_fmap_alterand removelist_alter_fmap_monowhich was a monomorphic duplicate.
With the exception of the list_elem_of_fmap change, all changes in this MR can be applied by sed. It would be best to merge it together with !526 (merged) so we only have to run a giant sed script once on reverse dependencies.
Edited by Robbert Krebbers