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.