diff --git a/theories/logrel/subtyping.v b/theories/logrel/subtyping.v
index 7bbceb0922e3db32edd867615f55c904bd867027..a436212beb73c0f3f3a9f8d9ca7fdd06cbb28724 100644
--- a/theories/logrel/subtyping.v
+++ b/theories/logrel/subtyping.v
@@ -197,6 +197,9 @@ Section subtype.
   Lemma lsty_le_refl P : ⊢ P <p: P.
   Proof. iApply iProto_le_refl. Qed.
 
+  Lemma lsty_le_trans P1 P2 P3 : P1 <p: P2 -∗ P2 <p: P3 -∗ P1 <p: P3.
+  Proof. iIntros "#H1 #H2 !>". by iApply iProto_le_trans. Qed.
+
   Lemma lsty_send_le A1 A2 P1 P2 :
     ▷ (A2 <: A1) -∗ ▷ (P1 <p: P2) -∗
     (<!!> A1 ; P1) <p: (<!!> A2 ; P2).