This is very experimental. It should now deal better with stuff like:

  match x with .. end = match y with .. end

In case there is a hypothesis H : R x y, it will try to destruct it.

Now, for example, when having equiv (Some x) (Some y) it will
try to find a Proper whose range is an equiv before hitting the
eq instance. My hack is general enough that it works for Forall2,
dist, and so on, too.

Thanks to Amin Timany for the suggestion.

Contrary to destruct_conj from Program.

It now turns setoid equalities into Leibniz equalities when possible,
and substitutes those.

In principle, we could now un-seal heap_mapsto, saved_prop_own etc., and mark them as "Typeclass Opaque", and ecancel would still work just as fast as it does now.
Thanks to Matthieu for pointing me to this unify feature.

This replaces f_equiv and solve_proper with our own, hopefully better, versions

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, make our redefinition of done more robust under different
orders of Importing modules.

Also do some minor clean up.