diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 37a9b4d786cc99f4605acbeb94ecc5a778ad19db..124966f739f3a186928fdb08c89e8a5312c6f49d 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -181,7 +181,8 @@ Section setoid.
     intros ?? Hf; apply partial_alter_proper.
     by destruct 1; constructor; apply Hf.
   Qed.
-  Lemma merge_ext f g `{!DiagNone f, !DiagNone g} :
+  Lemma merge_ext `{Equiv B, Equiv C} (f g : option A → option B → option C)
+      `{!DiagNone f, !DiagNone g} :
     ((≡) ==> (≡) ==> (≡))%signature f g →
     ((≡) ==> (≡) ==> (≡))%signature (merge (M:=M) f) (merge g).
   Proof.