Merge branch 'contractive' into 'master'

New definition of contractive.

The current notion of `Contractive` does not allow one to deal with functions with multiple arguments, for example, binary functions that are contractive in both arguments (like `lft_vs` in lambdarust), or binary functions that are contractive in one of their arguments.

To that end, I propose I reformulate the notion of `Contractive` so that we can express being contractive using a `Proper`. The new definition is:

    Definition dist_later {A : ofeT} (n : nat) (x y : A) : Prop :=
      match n with 0 => True | S n => x ≡{n}≡ y end.
    Notation Contractive f := (∀ n, Proper (dist_later n ==> dist n) f).

Also, it turns out that using this definition we can implement a `solve_contractive` tactic in the same way as the `solve_proper` tactic.

Unfortunately, the new tactic does not quite work for the weakest precondition connective in Iris because the proof involves induction, and the induction hypothesis does not quite fit into the new `solve_contractive` tactic.

See merge request !32