Better solvers for properness/contractiveness
solve_proper doesn't deal well with higher-order functions. Here's my home-grown variant:
(** An ad-hoc variant of solve_proper that seems to work better when defining
proper higher-order functions. In particular, using intro allows showing that a
lambda abstraction is proper if its body is proper.
Its implementation can also prove [f1 x ≡ f2 x] from [H : f1 ≡ f2]:
neither f_equiv nor rewrite deal with that, but [apply H] does. *)
Ltac solve_proper_ho_core tac :=
solve [repeat (tac (); cbn); cbn in *;
repeat match goal with H : _ ≡{_}≡ _|- _ => apply H end].
Ltac solve_proper_ho := solve_proper_ho_core
ltac:(fun _ => f_equiv || intro).
Ltac solve_contractive_ho := solve_proper_ho_core
ltac:(fun _ => f_contractive || f_equiv || intro).
Should we have something like this in Iris/stdpp? There's some heuristic tuning involved, but I use this rather happily...