diff --git a/heap_lang/heap.v b/heap_lang/heap.v
index d31ec3f44fa5e75cde4cc4ca31d1b568baee4fba..b01ed8e6151789f1f54530bab49fc141ed2b2d47 100644
--- a/heap_lang/heap.v
+++ b/heap_lang/heap.v
@@ -47,7 +47,7 @@ Section heap.
 
   (** Conversion to heaps and back *)
   Global Instance of_heap_proper : Proper ((≡) ==> (=)) of_heap.
-  Proof. by intros ??; fold_leibniz=>->. Qed.
+  Proof. solve_proper. Qed.
   Lemma from_to_heap σ : of_heap (to_heap σ) = σ.
   Proof.
     apply map_eq=>l. rewrite lookup_omap lookup_fmap. by case (σ !! l).
@@ -96,7 +96,7 @@ Section heap.
 
   (** Propers *)
   Global Instance heap_inv_proper : Proper ((≡) ==> (≡)) heap_inv.
-  Proof. intros h1 h2. by fold_leibniz=> ->. Qed.
+  Proof. solve_proper. Qed.
 
   (** General properties of mapsto *)
   Lemma heap_mapsto_disjoint l v1 v2 : (l ↦ v1 ★ l ↦ v2)%I ⊑ False.
diff --git a/prelude/tactics.v b/prelude/tactics.v
index fa51a99623e2833fccbba8c72b136ae282288fa4..1b96ec4f00d7267456078083398a7322a6e7db2c 100644
--- a/prelude/tactics.v
+++ b/prelude/tactics.v
@@ -188,6 +188,7 @@ Tactic Notation "simplify_eq" := repeat
   | H : ?x = _ |- _ => subst x
   | H : _ = ?x |- _ => subst x
   | H : _ = _ |- _ => discriminate H
+  | H : _ ≡ _ |- _ => apply leibniz_equiv in H
   | H : ?f _ = ?f _ |- _ => apply (inj f) in H
   | H : ?f _ _ = ?f _ _ |- _ => apply (inj2 f) in H; destruct H
     (* before [injection] to circumvent bug #2939 in some situations *)
@@ -237,7 +238,7 @@ Ltac f_equiv :=
   | |- pointwise_relation _ _ _ _ => intros ?
   end;
   (* Normalize away equalities. *)
-  subst;
+  simplify_eq;
   (* repeatedly apply congruence lemmas and use the equalities in the hypotheses. *)
   try match goal with
   | _ => first [ reflexivity | assumption | symmetry; assumption]