diff --git a/theories/logrel/session_types.v b/theories/logrel/session_types.v
index 0d78227cbc566b7d9196013cdf678ba4396899d3..1a79e7dc4da2a8896c31dd7a855f065001b538d1 100644
--- a/theories/logrel/session_types.v
+++ b/theories/logrel/session_types.v
@@ -83,7 +83,7 @@ Hint Mode LtyMsgTele ! - ! - - : typeclass_instances.
 Section session_types.
   Context {Σ : gFunctors}.
 
-  Global Instance lty_msg_exist_ne k :
+  Global Instance lty_msg_exist_ne k n :
     Proper (pointwise_relation _ (dist n) ==> (dist n)) (@lty_msg_exist Σ k).
   Proof. solve_proper. Qed.
   Global Instance lty_msg_exist_proper k :
@@ -107,11 +107,11 @@ Section session_types.
   Proof. solve_proper. Qed.
   Global Instance lty_choice_proper a : Proper ((≡) ==> (≡)) (@lty_choice Σ a).
   Proof. apply ne_proper, _. Qed.
-  Global Instance lty_choice_contractive a :
+  Global Instance lty_choice_contractive a n :
     Proper (map_relation (dist_later n) (λ _, False) (λ _, False) ==> dist n)
            (@lty_choice Σ a).
   Proof.
-    intros n Ss Ts Heq. rewrite /lty_choice.
+    intros Ss Ts Heq. rewrite /lty_choice.
     do 2 f_equiv. f_equiv => i.
     rewrite !lookup_total_alt.
     specialize (Heq i).
diff --git a/theories/logrel/subtyping.v b/theories/logrel/subtyping.v
index 2b94498e349307ed7c1c96726c3c85a61ed035c0..69acaac2ddcbf0ed0f7e33d7c22c68a8045e1e7c 100644
--- a/theories/logrel/subtyping.v
+++ b/theories/logrel/subtyping.v
@@ -34,7 +34,7 @@ Section subtyping.
   Global Instance lty_bi_le_plain {k} (M1 M2 : lty Σ k) : Plain (M1 <:> M2).
   Proof. rewrite /lty_bi_le /=. apply _. Qed.
 
-  Global Instance lty_le_ne : NonExpansive2 (@lty_le Σ k).
+  Global Instance lty_le_ne k : NonExpansive2 (@lty_le Σ k).
   Proof. destruct k; solve_proper. Qed.
   Global Instance lty_le_proper {k} : Proper ((≡) ==> (≡) ==> (≡)) (@lty_le Σ k).
   Proof. apply (ne_proper_2 _). Qed.