In particular, make sure we always try eassumption before reflexivity.

This has bothered me repeatedly in proofs, now I finally got around to fix it at the source

There is still the reals stuff, which is caused by importint Psatz (needed
for lia) and eq_rect_eq which is caused by importint Eqdep_dec.

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.

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.