This way we can use set_solver to solve goals involving ∈.

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

(These instances are not defined for any FinMap to avoid overlapping
instances for EqDecision, which may have awkward consequences for
type class search).

Having Is_true as a type class caused problems with rewrite: when the
rewrited lemma has a premise of the shape Is_true, the rewrite tactic
will complain that it cannot find a type class instance, instead
of generating a goal for that premise.

This also solves a name clash with the extension order of CMRAs.

This makes the typeclass mechanism able to use instances like [Is_true X -> Blah], where X reduces to X.

This happened for example in <[i:=x]>∅, where simpl unfold insert (despite
it being declared simpl never) because ∅ reduces to a constructor.

The previous commit is not really necesarry anymore, but my proof
for UIP of types with decidable equality is a bit more general, so
I won't revert it.

This way we get rid of the (unused) axiom eq_rect_eq reported by coqchk.

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.