diff --git a/algebra/fin_maps.v b/algebra/fin_maps.v
index 5310108636c09b16f622344e9964e56d30abf171..9b4817ff0b8a1db3dac5cb560ce84833d8842452 100644
--- a/algebra/fin_maps.v
+++ b/algebra/fin_maps.v
@@ -57,10 +57,8 @@ Proof.
     [by constructor|by apply lookup_ne].
 Qed.
 
-Global Instance map_timeless `{!∀ a : A, Timeless a} (g : gmap K A) : Timeless g.
-Proof.
-  intros m Hm i. apply timeless; eauto with typeclass_instances.
-Qed.
+Global Instance map_timeless `{∀ a : A, Timeless a} (m : gmap K A) : Timeless m.
+Proof. by intros m' ? i; apply (timeless _). Qed.
 
 Instance map_empty_timeless : Timeless (∅ : gmap K A).
 Proof.