diff --git a/theories/logrel/session_types.v b/theories/logrel/session_types.v
index 8466ecb96d1e53304868481412e236a99a7fec18..c9325512a6eb2e648e12227ca07dc6ffffa06065 100644
--- a/theories/logrel/session_types.v
+++ b/theories/logrel/session_types.v
@@ -94,8 +94,8 @@ Section session_types.
   Global Instance lty_msg_base_proper :
     Proper ((≡) ==> (≡) ==> (≡)) (@lty_msg_base Σ).
   Proof. rewrite /lty_msg_base. apply ne_proper_2, _. Qed.
-  Global Instance lty_msg_base_contractive n A :
-    Proper (dist_later n ==> dist n) (@lty_msg_base Σ A).
+  Global Instance lty_msg_base_contractive n :
+    Proper (dist n ==> dist_later n ==> dist n) (@lty_msg_base Σ).
   Proof. solve_contractive. Qed.
 
   Global Instance lty_message_ne a : NonExpansive (@lty_message Σ a).
diff --git a/theories/logrel/term_types.v b/theories/logrel/term_types.v
index b2ab312f4ce6f6bb71a0c21c676ae6fb2a7ef5ff..c6307222ab1713cc3f192a6a3006ff8963c099d7 100644
--- a/theories/logrel/term_types.v
+++ b/theories/logrel/term_types.v
@@ -157,6 +157,8 @@ Section term_types.
   Global Instance lty_ref_shr_ne `{heapG Σ} : NonExpansive lty_ref_shr.
   Proof. solve_proper. Qed.
 
+  Global Instance lty_chan_contractive `{heapG Σ, chanG Σ} : Contractive lty_chan.
+  Proof. solve_contractive. Qed.
   Global Instance lty_chan_ne `{heapG Σ, chanG Σ} : NonExpansive lty_chan.
   Proof. solve_proper. Qed.
 End term_types.