Some `filter` lemmas make use of `map_Forall`, so put `map_Forall` before `filter.

Introduce `set_bind` and associated lemmas + set_bind theory: revise setoid rewriting

See merge request iris/stdpp!406

- strengthen set_bind_subset to have the same arity
- add missing Params instance to prevent slow failures in setoid rewriting
- `Proper` instances can be proven before `set_bind_ext` via `set_solver`.
- `set_bind_ext` is then provable by set_solver directly.

Add map_seqZ

See merge request iris/stdpp!391

Add _1, _2 lemmas for not_elem_of_dom and lookup_union_None

See merge request iris/stdpp!405

Add lookup_union_l'

See merge request iris/stdpp!395

Add map_agree

See merge request iris/stdpp!392

Flip direction of `map_disjoint_fmap`.

See merge request iris/stdpp!398

Add list_subseteq_dec

See merge request iris/stdpp!400

Add lookup lemmas for partial alter and commuting lemmas for alter

See merge request iris/stdpp!399

Add join_length

See merge request iris/stdpp!401

Add case_match eqn: tactic for naming hypotheses generated by case_match

See merge request iris/stdpp!388

Add map_Exists

See merge request iris/stdpp!390

Fix the naming of kmap_subseteq and kmap_subset

See merge request iris/stdpp!393