Drop `DiagNone` precondition of `lookup_merge` rule of `FinMap` interface.

Closes #94

See merge request !279

Misc setoids lemmas and tweaks for maps and option

See merge request iris/stdpp!276

Add `Proper`s for maps, and generalise existing ones. Add tests to check that the old ones can be derived.

Rename `option_mbind_proper` → `option_bind_proper` and `option_mjoin_proper` → `option_join_proper`.

Make filter lemmas for maps and sets consistent + add cross split property for maps

See merge request !274

Rename `map_disjoint_filter` → `map_disjoint_filter_complement` and `map_union_filter` → `map_filter_union_complement`.

sum_list_with_in

See merge request !275

Strengthen `map_filter_strong_ext` and `map_filter_ext`.

See merge request !269