This class whose name is horrible and purpose is arbitrary seems to be a
leftover of some experiment with ch2o, a long time a ago.

It now traverses terms at most once, whereas the setoid_rewrite
approach was travering terms many times. Also, the tactic can now
be extended by defining type class instances.

Also, use "set_solver by tac" to specify a tactic.

In most cases there is a lot of duplicate proof search performed by
both naive_solver and eauto. Especially since naive_solver calls its
tactic (in the case of set_solver this used to be eauto) quite eagerly
this made it very slow.

Note that set_solver is this too slow and should be improved.

In most cases there is a lot of duplicate proof search performed by
both naive_solver and eauto. Especially since naive_solver calls its
tactic (in the case of set_solver this used to be eauto) quite eagerly
this made it very slow.

Note that set_solver is this too slow and should be improved.

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.

Also, make our redefinition of done more robust under different
orders of Importing modules.

This one (previously solve_elem_of) was hardly used. The tactic that uses
naive_solver (previously esolve_elem_of, now solve_elem_of) has been
extended with flags to say which hypotheses should be cleared/kept.

* Remove the order from RAs, it is now defined in terms of the ⋅ operation.
* Define ownership using the step-indexed order.
* Remove the order also from DRAs and change STS accordingly. While doing
  that, I changed STS to no longer use decidable token sets, which removes the
  requirement of decidable equality on tokens.

The port makes the following notable changes:

* The carrier types of separation algebras and integer environments are no
  longer in Set. Now they have a type at a fixed type level above Set. This
  both works better in 8.5 and makes the formalization more general.
  I have tried putting them at polymorphic type levels, but that increased the
  compilation time by an order of magnitude.
* I am using a custom f_equal tactic written in Ltac to circumvent bug #4069.
  That bug has been fixed, so this custom tactic can be removed when the next
  beta of 8.5 is out.