diff --git a/theories/gmultiset.v b/theories/gmultiset.v
index f0fa7ffb1934914d064f3667e761df121d431a95..6940ba8e581f08ef73bedb5260df9e1bf227a769 100644
--- a/theories/gmultiset.v
+++ b/theories/gmultiset.v
@@ -222,7 +222,7 @@ Proof.
   rewrite !multiplicity_disj_union. lia.
 Qed.
 Global Instance gmultiset_disj_union_inj_2 X : Inj (=) (=) (.⊎ X).
-Proof. intros Y1 Y2. rewrite <-!(comm_L _ X). apply (inj _). Qed.
+Proof. intros Y1 Y2. rewrite <-!(comm_L _ X). apply (inj (X ⊎.)). Qed.
 
 Lemma gmultiset_disj_union_intersection_l X Y Z : X ⊎ (Y ∩ Z) = (X ⊎ Y) ∩ (X ⊎ Z).
 Proof.
diff --git a/theories/list.v b/theories/list.v
index 1203a5db8a9052755862aa9ff5f4e8e283787e9e..825b2f096781100bece52fbdcccec567b5740d65 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -2232,7 +2232,7 @@ Qed.
 Lemma submseteq_app_inv_l l1 l2 k : k ++ l1 ⊆+ k ++ l2 → l1 ⊆+ l2.
 Proof.
   induction k as [|y k IH]; simpl; [done |]. rewrite submseteq_cons_l.
-  intros (?&E%(inj _)&?). apply IH. by rewrite E.
+  intros (?&E%(inj (cons y))&?). apply IH. by rewrite E.
 Qed.
 Lemma submseteq_app_inv_r l1 l2 k : l1 ++ k ⊆+ l2 ++ k → l1 ⊆+ l2.
 Proof.
diff --git a/theories/numbers.v b/theories/numbers.v
index 8f2914358c461010faf97feafd6269fdc4c9c3a1..6f03dd236605a1b260d920590d220d85413b8d68 100644
--- a/theories/numbers.v
+++ b/theories/numbers.v
@@ -710,7 +710,7 @@ Proof. intros x y z; apply Qp_eq, Qcplus_assoc. Qed.
 Instance Qp_plus_comm : Comm (=) Qp_plus.
 Proof. intros x y; apply Qp_eq, Qcplus_comm. Qed.
 Instance Qp_plus_inj_r p : Inj (=) (=) (Qp_plus p).
-Proof. intros q1 q2. rewrite !Qp_eq; simpl. apply (inj _). Qed.
+Proof. intros q1 q2. rewrite !Qp_eq; simpl. apply (inj (Qcplus p)). Qed.
 Instance Qp_plus_inj_l p : Inj (=) (=) (λ q, q + p)%Qp.
 Proof. intros q1 q2. rewrite !Qp_eq; simpl. apply (inj (λ q, q + p)%Qc). Qed.
 
@@ -794,9 +794,9 @@ Proof.
     destruct (Qclt_le_dec a c) as [?|[?| ->%Qp_eq]%Qcle_lt_or_eq].
     - auto.
     - destruct (help c d a b); [done..|]. naive_solver.
-    - apply (inj _) in H as ->. destruct (Qp_lower_bound a d) as (q&a'&d'&->&->).
+    - apply (inj (Qp_plus a)) in H as ->. destruct (Qp_lower_bound a d) as (q&a'&d'&->&->).
       eauto 10 using (comm_L Qp_plus). }
-  intros a b c d [e ->]%Qp_lt_sum. rewrite <-(assoc_L _). intros ->%(inj _).
+  intros a b c d [e ->]%Qp_lt_sum. rewrite <-(assoc_L _). intros ->%(inj (Qp_plus a)).
   destruct (Qp_lower_bound a d) as (q&a'&d'&->&->).
   eexists a', q, (q + e)%Qp, d'; split_and?; auto using (comm_L Qp_plus).
   - by rewrite (assoc_L _), (comm_L Qp_plus e).