diff --git a/theories/algebra/cmra.v b/theories/algebra/cmra.v
index 8fbfcdddfa02c4574001230dd46b3e094507057c..f302796bebbbfd4714d1d8a602d923ff8c423297 100644
--- a/theories/algebra/cmra.v
+++ b/theories/algebra/cmra.v
@@ -622,7 +622,7 @@ Qed.
 Global Instance id_free_op_r x y : IdFree y → Cancelable x → IdFree (x ⋅ y).
 Proof.
   intros ?? z ? Hid%symmetry. revert Hid. rewrite -assoc=>/(cancelableN x) ?.
-  eapply (id_free0_r _); [by eapply cmra_validN_op_r |symmetry; eauto].
+  eapply (id_free0_r y); [by eapply cmra_validN_op_r |symmetry; eauto].
 Qed.
 Global Instance id_free_op_l x y : IdFree x → Cancelable y → IdFree (x ⋅ y).
 Proof. intros. rewrite comm. apply _. Qed.