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.