I added the old one in 176a588c but it was never used.

Using this new definition we can express being contractive using a
Proper. This has the following advantages:

- It makes it easier to state that a function with multiple arguments
  is contractive (in all or some arguments).
- A solve_contractive tactic can be implemented by extending the
  solve_proper tactic.

This removes Ralf's hack of using later_car, which is not function in the logic.

Thanks to Aleš for suggesting this.

The rewrite auth_validN_eq was not performed in the hypothesis. It
used to work in 8.5 because of magic.

Also, use explicit unfolding lemmas for auth_valid and auth_validN.
The `Arguments valid _ _ !_ /` hack did not really work when one
has to deal with the valid instance of the cmra, which underneath also
includes a `cmra_valid`. Declaring a similar Arguments for `cmra_valid`
is a bad idea, it will also end up unfold stuff for the exclusive and
option CMRA.

This fixes issue #46.

Proof was done by Hai & me

Use COFEs only for the recursive domain equation solver

Many useful properties are probably still missing.

And also rename the corresponding proof mode tactics.

Initial proof by Jan-Oliver Kaiser, adapted by Robbert Krebbers.

Initial proof by Jan-Oliver Kaiser, adapted by Robbert Krebbers.