It is doing much more than just dealing with ∈, it solves all kinds
of goals involving set operations (including ≡ and ⊆).

simplify_equality        => simplify_eq
simplify_equality'       => simplify_eq/=
simplify_map_equality    => simplify_map_eq
simplify_map_equality'   => simplify_map_eq/=
simplify_option_equality => simplify_option_eq
simplify_list_equality   => simplify_list_eq
f_equal'                 => f_equal/=

The /= suffixes (meaning: do simpl) are inspired by ssreflect.

The tactic injection H as H is doing exactly that.

Also, specialize the big ops to gmap and gset because that is all that
we are using. For the big ops on sets this also means we can use Leibniz
equality on sets.

Do not use proper explicitly but let setoids handle it.

This prevent the assumption from being dragged into lemmas that do not even need it

The singleton maps notation is now also more consistent with the
insert <[_ := _]> _ notation for maps.

Now that there is more of it, it deserves its own place :).

Also, put stuff in a section.