diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index bfbc2eebfb5f97344475e5fc6239650d9b16c902..0453473c771a488bb4cd173409e894367083108c 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -570,9 +570,7 @@ Qed.
 Lemma insert_subseteq_l {A} (m1 m2 : M A) i x :
   m2 !! i = Some x → m1 ⊆ m2 → <[i:=x]> m1 ⊆ m2.
 Proof.
-  intros Hi Hincl. replace m2 with (<[i:=x]> m2).
-  - apply insert_mono. done.
-  - apply insert_id. done.
+  intros Hi Hincl. etrans; [apply insert_mono, Hincl|]. by rewrite insert_id.
 Qed.
 
 Lemma insert_delete_subseteq {A} (m1 m2 : M A) i x :