diff --git a/theories/logrel/session_types.v b/theories/logrel/session_types.v
index cb8dcc263d5e894f5259e2d20f84ab3e5c6a02b1..8289817c72d32b6d31fffbfd4967886e2e11b04d 100644
--- a/theories/logrel/session_types.v
+++ b/theories/logrel/session_types.v
@@ -64,19 +64,14 @@ Section session_types.
   Global Instance lty_msg_exist_proper k :
     Proper (pointwise_relation _ (≡) ==> (≡)) (@lty_msg_exist Σ k).
   Proof. solve_proper. Qed.
-  Global Instance lty_msg_base_ne a : NonExpansive2 (@lty_msg_base Σ a).
+  Global Instance lty_msg_base_ne : NonExpansive2 (@lty_msg_base Σ).
   Proof. rewrite /lty_msg_base. solve_proper. Qed.
-  Global Instance lty_msg_base_proper a :
-    Proper ((≡) ==> (≡) ==> (≡)) (@lty_msg_base Σ a).
+  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 :
     Proper (dist_later n ==> dist_later n ==> dist n) (@lty_msg_base Σ).
-  Proof.
-    intros A1 A2 HA S1 S2 HS.
-    rewrite /lty_msg_base.
-    f_equiv=> w.
-    by repeat f_contractive.
-  Qed.
+  Proof. solve_contractive. Qed.
 
   Global Instance lty_message_ne a : NonExpansive (@lty_message Σ a).
   Proof. solve_proper. Qed.