diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 654c7acf7b7b49b63ae3427bfa5c295b62ddb51c..577a3c0778796aa3a449c7799b4ffa76772b9f80 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -2394,14 +2394,14 @@ Global Instance map_difference_right_id {A} : RightId (=) (∅:M A) (∖) := _.
 Lemma map_difference_empty {A} (m : M A) : m ∖ ∅ = m.
 Proof. by rewrite (right_id _ _). Qed.
 
-Lemma map_delete_difference {A} (m1 m2 : M A) i x :
+Lemma delete_difference {A} (m1 m2 : M A) i x :
   delete i (m1 ∖ m2) = m1 ∖ <[i:=x]> m2.
 Proof.
   apply map_eq. intros j. apply option_eq. intros y.
   rewrite lookup_delete_Some, !lookup_difference_Some, lookup_insert_None.
   naive_solver.
 Qed.
-Lemma map_difference_delete {A} (m1 m2 : M A) i x :
+Lemma difference_delete {A} (m1 m2 : M A) i x :
   m1 !! i = Some x →
   m1 ∖ delete i m2 = <[i:=x]> (m1 ∖ m2).
 Proof.