Extend `solve_proper` to better handle HO functions

See the report here: iris#249 (closed)

I ran into a problem that's related in @dfrumin's ReLoC reloc@3266aca9

mentioned in issue iris#249 (closed)

This problem also appears in Iris: https://gitlab.mpi-sws.org/iris/iris/blob/master/theories/program_logic/weakestpre.v#L39

This proof should be handled automatically.

mentioned in issue #8

For the record, my current "HO" solver is now the following, which is much better than the one in iris#249 (closed) — tho this one is Iris-specific.

Ltac ho_f_equiv :=
  progress repeat match goal with
    | H : _ ≡ _|- _ => (apply: H || rewrite H //)
    | H : _ ≡{_}≡ _ |- _ => (apply: H || rewrite H //)
    | H : dist_later _ _ _ |- _ => (apply: H || rewrite H //)
    end.

Ltac solve_proper_ho := solve_proper_core ltac:(fun _ => ho_f_equiv || f_equiv).
Ltac solve_contractive_ho := solve_proper_core ltac:(fun _ => ho_f_equiv || f_contractive || f_equiv).

Here we accept dist_later, instead of simplifying all assumptions and using equalities, like in iris#249 (closed).