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.

This is a workarround, see: https://github.com/math-comp/math-comp/issues/18

This way, they are non-delta unfoldable constants, which showed a positive
impact on the performance of setoid rewriting. We may want to do this for
other cmra/cofe structures too.

These are hardly used, and confusing since we have so many operations of
different arities that distribute.

Sadly, timelessness of many connectives is still proved in the model.

Now we use a specific notation (⊑) to whose arguments we interpret
in uPred_scope. This makes notations much more concise.

These are unused and not very useful anymore now that we have gmap.