diff git a/theories/gmultiset.v b/theories/gmultiset.v
index e27d03fac21b13d571a58f27efef53b9f69f698f..27db25b3cbbb6cbb26182d38bf0050f400d87733 100644
 a/theories/gmultiset.v
+++ b/theories/gmultiset.v
@@ 185,8 +185,8 @@ Proof.
rewrite !map_to_list_insert, !bind_cons
by (by rewrite ?lookup_union_with, ?lookup_delete, ?HX).
rewrite (assoc_L _), <(comm (++) (f (_,n'))), <!(assoc_L _), <IH.
 rewrite (assoc_L _); f_equiv; [rewrite (comm _); simpldone].
 by rewrite replicate_plus, Permutation_middle.
+ rewrite (assoc_L _). f_equiv.
+ rewrite (comm _); simpl. by rewrite replicate_plus, Permutation_middle.
 rewrite <insert_union_with_l, !map_to_list_insert, !bind_cons
by (by rewrite ?lookup_union_with, ?HX, ?HY).
by rewrite <(assoc_L (++)), <IH.
diff git a/theories/tactics.v b/theories/tactics.v
index 807d1159c3c1499f2ea20d5100f6065591829171..5c8199a5bfaf52a098996c1952ad0a48687490a4 100644
 a/theories/tactics.v
+++ b/theories/tactics.v
@@ 273,6 +273,7 @@ favor the second because the relation (dist) stays the same. *)
Ltac f_equiv :=
match goal with
 _ => reflexivity
+   pointwise_relation _ _ _ _ => intros ?
(* We support matches on both sides, *if* they concern the same variable, or
variables in some relation. *)
  ?R (match ?x with _ => _ end) (match ?x with _ => _ end) =>
@@ 301,26 +302,12 @@ Ltac f_equiv :=
(* In case the function symbol differs, but the arguments are the same,
maybe we have a pointwise_relation in our context. *)
 H : pointwise_relation _ ?R ?f ?g  ?R (?f ?x) (?g ?x) => apply H
 end.

(** auto_proper solves goals of the form "f _ = f _", for any relation and any
 number of arguments, by repeatedly applying f_equiv and handling trivial cases.
 If it cannot solve an equality, it will leave that to the user. *)
Ltac auto_equiv :=
 (* Deal with "pointwise_relation" *)
 repeat lazymatch goal with
   pointwise_relation _ _ _ _ => intros ?
end;
 (* Normalize away equalities. *)
 simplify_eq;
 (* repeatedly apply congruence lemmas and use the equalities in the hypotheses. *)
 try (f_equiv; fast_done  auto_equiv).

(** solve_proper solves goals of the form "Proper (R1 ==> R2)", for any
 number of relations. All the actual work is done by auto_equiv;
 solve_proper just introduces the assumptions and unfolds the first
 head symbol. *)
Ltac solve_proper :=
+ try reflexivity.
+
+(* The tactic [preprocess_solve_proper] unfolds the first head symbol, so that
+we proceed by repeatedly using [f_equiv]. *)
+Ltac preprocess_solve_proper :=
(* Introduce everything *)
intros;
repeat lazymatch goal with
@@ 340,7 +327,14 @@ Ltac solve_proper :=
  ?R (?f _ _) (?f _ _) => unfold f
  ?R (?f _) (?f _) => unfold f
end;
 solve [ auto_equiv ].
+ simplify_eq.
+
+(** The tactic [solve_proper] solves goals of the form "Proper (R1 ==> R2)", for
+any number of relations. The actual work is done by repeatedly applying
+[f_equiv]. *)
+Ltac solve_proper :=
+ preprocess_solve_proper;
+ solve [repeat (f_equiv; try eassumption)].
(** The tactic [intros_revert tac] introduces all foralls/arrows, performs tac,
and then reverts them. *)