diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index aa75c29d05ede015211e0b72cf98ee905b64a998..694b9ec089b7555fae214266205925fdc30182c5 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -977,8 +977,8 @@ Qed.
 
 Global Instance map_eq_dec_empty {A} (m : M A) : Decision (m = ∅) | 20.
 Proof.
-  refine (cast_if (decide (elements m = [])));
-    [apply _|by rewrite <-?map_to_list_empty' ..].
+  refine (cast_if (decide (map_to_list m = [])));
+    by rewrite <-?map_to_list_empty'.
 Defined.
 
 (** Properties of the imap function *)