Uncurried contractiveness of lty_msg_base, and added contractive of lty_chan

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).

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.