diff --git a/theories/logrel/session_types.v b/theories/logrel/session_types.v
index 5ea8484fd1300e204f85ba715d324c0c19f5f501..2e187d946e9874b26e47e625b5e61a8d15a91adf 100644
--- a/theories/logrel/session_types.v
+++ b/theories/logrel/session_types.v
@@ -164,4 +164,8 @@ Section session_types.
     do 4 f_equiv. by rewrite iMsg_app_base.
   Qed.
 
+  Lemma lsty_car_app (S T : lsty Σ) :
+    (lsty_car S <++> lsty_car T)%proto ≡ lsty_car (S <++> T).
+  Proof. eauto. Qed.
+
 End session_types.
diff --git a/theories/logrel/subtyping.v b/theories/logrel/subtyping.v
index 6a7c3c941b5c5d342c71a7af180fff95af5361dc..dc6c23529bee7e0d6eabd8aa757a99bea615cdbc 100644
--- a/theories/logrel/subtyping.v
+++ b/theories/logrel/subtyping.v
@@ -45,4 +45,9 @@ Section subtyping.
   Proof. rewrite /lty_copyable /=. apply _. Qed.
   Global Instance lty_copyable_ne : NonExpansive (@lty_copyable Σ).
   Proof. rewrite /lty_copyable /=. solve_proper. Qed.
+
+  Lemma lsty_car_mono (S T : lsty Σ) :
+    (S <: T) -∗ lsty_car S ⊑ lsty_car T.
+  Proof. eauto. Qed.
+
 End subtyping.