diff --git a/theories/logrel/subtyping.v b/theories/logrel/subtyping.v
index 6fe83188344759ad9ce09aaefc8634feaa59b3db..8da5498ce093f14b39cfb43c3288db98f3b71541 100644
--- a/theories/logrel/subtyping.v
+++ b/theories/logrel/subtyping.v
@@ -56,9 +56,9 @@ Section subtype.
 
   Lemma lty_bi_le_refl A : ⊢ A <:> A.
   Proof. iSplit; iApply lty_le_refl. Qed.
-  Lemma lty_bi_le_trans A1 A2 A3 : ⊢ A1 <:> A2 -∗ A2 <:> A3 -∗ A1 <:> A3.
+  Lemma lty_bi_le_trans A1 A2 A3 : A1 <:> A2 -∗ A2 <:> A3 -∗ A1 <:> A3.
   Proof. iIntros "#[H11 H12] #[H21 H22]". iSplit; by iApply lty_le_trans. Qed.
-  Lemma lty_bi_le_sym A1 A2 : ⊢ A1 <:> A2 -∗ A2 <:> A1.
+  Lemma lty_bi_le_sym A1 A2 : A1 <:> A2 -∗ A2 <:> A1.
   Proof. iIntros "[$$]". Qed.
 
   Lemma lty_le_copy A : ⊢ copy A <: A.
@@ -201,9 +201,9 @@ Section subtype.
 
   Lemma lsty_bi_le_refl S : ⊢ S <s:> S.
   Proof. iSplit; iApply lsty_le_refl. Qed.
-  Lemma lsty_bi_le_trans S1 S2 S3 : ⊢ S1 <s:> S2 -∗ S2 <s:> S3 -∗ S1 <s:> S3.
+  Lemma lsty_bi_le_trans S1 S2 S3 : S1 <s:> S2 -∗ S2 <s:> S3 -∗ S1 <s:> S3.
   Proof. iIntros "#[H11 H12] #[H21 H22]". iSplit; by iApply lsty_le_trans. Qed.
-  Lemma lsty_bi_le_sym S1 S2 : ⊢ S1 <s:> S2 -∗ S2 <s:> S1.
+  Lemma lsty_bi_le_sym S1 S2 : S1 <s:> S2 -∗ S2 <s:> S1.
   Proof. iIntros "[$$]". Qed.
 
   Lemma lsty_le_send A1 A2 S1 S2 :