diff --git a/theories/logrel/subtyping.v b/theories/logrel/subtyping.v
index 428b13a2443ecf2cfdc07fcf28537c75fe179d20..3ebdbedd8fdad2eea23decbe2fd4fa6a4cc19d36 100644
--- a/theories/logrel/subtyping.v
+++ b/theories/logrel/subtyping.v
@@ -6,10 +6,17 @@ equivalent to having both [A <: B] and [B <: A]. Finally, the notion of a
 when [A <: copy A]. *)
 From actris.logrel Require Export model term_types.
 
+Definition lsty_le_def {Î£} (P1 P2 : lsty Î£) :=
+  iProto_le (lsty_car P1) (lsty_car P2).
+Definition lsty_le_aux : seal (@lsty_le_def). by eexists. Qed.
+Definition lsty_le := lsty_le_aux.(unseal).
+Definition lsty_le_eq : @lsty_le = @lsty_le_def := lsty_le_aux.(seal_eq).
+Arguments lsty_le {_} _ _.
+
 Definition lty_le {Î£ k} : lty Î£ k â†’ lty Î£ k â†’ iProp Î£ :=
   match k with
   | tty_kind => Î» A1 A2, â–  âˆ€ v, ltty_car A1 v -âˆ— ltty_car A2 v
-  | lty_kind => Î» P1 P2, â–  iProto_le (lsty_car P1) (lsty_car P2)
+  | lty_kind => Î» P1 P2, â–  lsty_le P1 P2
   end%I.
 Arguments lty_le : simpl never.
 Infix "<:" := lty_le (at level 70) : bi_scope.
@@ -34,7 +41,9 @@ Section subtyping.
   Proof. rewrite /lty_bi_le /=. apply _. Qed.
 
   Global Instance lty_le_ne : NonExpansive2 (@lty_le Î£ k).
-  Proof. destruct k; solve_proper. Qed.
+  Proof.
+    rewrite /lty_le lsty_le_eq. destruct k; rewrite ?/lsty_le_def; solve_proper.
+  Qed.
   Global Instance lty_le_proper {k} : Proper ((â‰¡) ==> (â‰¡) ==> (â‰¡)) (@lty_le Î£ k).
   Proof. apply (ne_proper_2 _). Qed.
   Global Instance lty_bi_le_ne {k} : NonExpansive2 (@lty_bi_le Î£ k).
diff --git a/theories/logrel/subtyping_rules.v b/theories/logrel/subtyping_rules.v
index 75a170d0800c058037ffa19fb8f5a16f82281456..d91dd81fa20d964d5a138e424c8cd2f4c69981d1 100644
--- a/theories/logrel/subtyping_rules.v
+++ b/theories/logrel/subtyping_rules.v
@@ -12,12 +12,14 @@ Section subtyping_rules.
 
   (** Generic rules *)
   Lemma lty_le_refl {k} (M : lty Î£ k) : âŠ¢ M <: M.
-  Proof. destruct k. by iIntros (v) "!> H". by iModIntro. Qed.
+  Proof. destruct k. by iIntros (v) "!> H".
+         rewrite /lty_le lsty_le_eq /lsty_le_def. by iModIntro. Qed.
   Lemma lty_le_trans {k} (M1 M2 M3 : lty Î£ k) : M1 <: M2 -âˆ— M2 <: M3 -âˆ— M1 <: M3.
   Proof.
     destruct k.
     - iIntros "#H1 #H2" (v) "!> H". iApply "H2". by iApply "H1".
-    - iIntros "#H1 #H2 !>". by iApply iProto_le_trans.
+    - iIntros "#H1 #H2 !>".
+      rewrite /lty_le lsty_le_eq /lsty_le_def. by iApply iProto_le_trans.
   Qed.
 
   Lemma lty_bi_le_refl {k} (M : lty Î£ k) : âŠ¢ M <:> M.
@@ -242,7 +244,8 @@ Section subtyping_rules.
     â–· (S1 <: S2) -âˆ— chan S1 <: chan S2.
   Proof.
     iIntros "#Hle" (v) "!> H".
-    iApply (iProto_mapsto_le with "H [Hle]"). eauto.
+    iApply (iProto_mapsto_le with "H [Hle]").
+    rewrite /lty_le lsty_le_eq. eauto.
   Qed.
 
   (** Session subtyping *)
@@ -250,6 +253,7 @@ Section subtyping_rules.
     â–· (A2 <: A1) -âˆ— â–· (S1 <: S2) -âˆ—
     (<!!> TY A1 ; S1) <: (<!!> TY A2 ; S2).
   Proof.
+    rewrite /lty_le lsty_le_eq.
     iIntros "#HAle #HSle !>" (v) "H". iExists v.
     iDestruct ("HAle" with "H") as "$". by iModIntro.
   Qed.
@@ -258,6 +262,7 @@ Section subtyping_rules.
     â–· (A1 <: A2) -âˆ— â–· (S1 <: S2) -âˆ—
     (<??> TY A1 ; S1) <: (<??> TY A2 ; S2).
   Proof.
+    rewrite /lty_le lsty_le_eq.
     iIntros "#HAle #HSle !>" (v) "H". iExists v.
     iDestruct ("HAle" with "H") as "$". by iModIntro.
   Qed.
@@ -265,22 +270,33 @@ Section subtyping_rules.
   Lemma lty_le_exist_elim_l k (M : lty Î£ k â†’ lmsg Î£) S :
     (âˆ€ (A : lty Î£ k), (<??> M A) <: S) -âˆ—
     ((<?? (A : lty Î£ k)> M A) <: S).
-  Proof. iIntros "#Hle !>". iApply (iProto_le_exist_elim_l_inhabited M). auto. Qed.
+  Proof.
+    rewrite /lty_le lsty_le_eq.
+    iIntros "#Hle !>". iApply (iProto_le_exist_elim_l_inhabited M). auto.
+  Qed.
 
   Lemma lty_le_exist_elim_r k (M : lty Î£ k â†’ lmsg Î£) S :
     (âˆ€ (A : lty Î£ k), S <: (<!!> M A)) -âˆ—
     (S <: (<!! (A : lty Î£ k)> M A)).
-  Proof. iIntros "#Hle !>". iApply (iProto_le_exist_elim_r_inhabited _ M). auto. Qed.
+  Proof.
+    rewrite /lty_le lsty_le_eq.
+    iIntros "#Hle !>". iApply (iProto_le_exist_elim_r_inhabited _ M). auto.
+  Qed.
 
   Lemma lty_le_exist_intro_l k (M : lty Î£ k â†’ lmsg Î£) (A : lty Î£ k) :
     âŠ¢ (<!! X> M X) <: (<!!> M A).
-  Proof. iIntros "!>". iApply (iProto_le_exist_intro_l). Qed.
+  Proof.
+    rewrite /lty_le lsty_le_eq.
+    iIntros "!>". iApply (iProto_le_exist_intro_l).
+  Qed.
 
   Lemma lty_le_exist_intro_r k (M : lty Î£ k â†’ lmsg Î£) (A : lty Î£ k) :
     âŠ¢ (<??> M A) <: (<?? X> M X).
-  Proof. iIntros "!>". iApply (iProto_le_exist_intro_r). Qed.
+  Proof.
+    rewrite /lty_le lsty_le_eq.
+    iIntros "!>". iApply (iProto_le_exist_intro_r).
+  Qed.
 
-  (* Elimination rules need inhabited variant of telescopes in the model *)
   Lemma lty_le_texist_elim_l {kt} (M : ltys Î£ kt â†’ lmsg Î£) S :
     (âˆ€ Xs, (<??> M Xs) <: S) -âˆ—
     (<??.. Xs> M Xs) <: S.
@@ -316,6 +332,7 @@ Section subtyping_rules.
   Lemma lty_le_swap_recv_send A1 A2 S :
     âŠ¢ (<??> TY A1; <!!> TY A2; S) <: (<!!> TY A2; <??> TY A1; S).
   Proof.
+    rewrite /lty_le lsty_le_eq.
     iIntros "!>" (v1 v2).
     iApply iProto_le_trans;
       [iApply iProto_le_base; iApply (iProto_le_exist_intro_l _ v2)|].
@@ -327,6 +344,7 @@ Section subtyping_rules.
   Lemma lty_le_swap_recv_select A Ss :
     âŠ¢ (<??> TY A; lty_select Ss) <: lty_select ((Î» S, <??> TY A; S) <$> Ss)%lty.
   Proof.
+    rewrite /lty_le lsty_le_eq.
     iIntros "!>" (v1 x2).
     iApply iProto_le_trans;
       [iApply iProto_le_base; iApply (iProto_le_exist_intro_l _ x2)|]; simpl.
@@ -340,6 +358,7 @@ Section subtyping_rules.
   Lemma lty_le_swap_branch_send A Ss :
     âŠ¢ lty_branch ((Î» S, <!!> TY A; S) <$> Ss)%lty <: (<!!> TY A; lty_branch Ss).
   Proof.
+    rewrite /lty_le lsty_le_eq.
     iIntros "!>" (x1 v2).
     iApply iProto_le_trans;
       [|iApply iProto_le_base; iApply (iProto_le_exist_intro_r _ x1)]; simpl.
@@ -354,6 +373,7 @@ Section subtyping_rules.
     â–· ([âˆ— map] S1;S2 âˆˆ Ss1; Ss2, S1 <: S2) -âˆ—
     lty_select Ss1 <: lty_select Ss2.
   Proof.
+    rewrite /lty_le lsty_le_eq.
     iIntros "#H !>" (x); iMod 1 as %[S2 HSs2]. iExists x.
     iDestruct (big_sepM2_forall with "H") as "{H} [>% H]".
     assert (is_Some (Ss1 !! x)) as [S1 HSs1] by naive_solver.
@@ -365,6 +385,7 @@ Section subtyping_rules.
     Ss2 âŠ† Ss1 â†’
     âŠ¢ lty_select Ss1 <: lty_select Ss2.
   Proof.
+    rewrite /lty_le lsty_le_eq.
     intros; iIntros "!>" (x); iMod 1 as %[S HSs2]. iExists x.
     assert (Ss1 !! x = Some S) as HSs1 by eauto using lookup_weaken.
     rewrite HSs1. iSplitR; [by eauto|].
@@ -375,6 +396,7 @@ Section subtyping_rules.
     â–· ([âˆ— map] S1;S2 âˆˆ Ss1; Ss2, S1 <: S2) -âˆ—
     lty_branch Ss1 <: lty_branch Ss2.
   Proof.
+    rewrite /lty_le lsty_le_eq.
     iIntros "#H !>" (x); iMod 1 as %[S1 HSs1]. iExists x.
     iDestruct (big_sepM2_forall with "H") as "{H} [>% H]".
     assert (is_Some (Ss2 !! x)) as [S2 HSs2] by naive_solver.
@@ -386,6 +408,7 @@ Section subtyping_rules.
     Ss1 âŠ† Ss2 â†’
     âŠ¢ lty_branch Ss1 <: lty_branch Ss2.
   Proof.
+    rewrite /lty_le lsty_le_eq.
     intros; iIntros "!>" (x); iMod 1 as %[S HSs1]. iExists x.
     assert (Ss2 !! x = Some S) as HSs2 by eauto using lookup_weaken.
     rewrite HSs2. iSplitR; [by eauto|].
@@ -396,25 +419,29 @@ Section subtyping_rules.
   Lemma lty_le_app S11 S12 S21 S22 :
     (S11 <: S21) -âˆ— (S12 <: S22) -âˆ—
     (S11 <++> S12) <: (S21 <++> S22).
-  Proof. iIntros "#H1 #H2 !>". by iApply iProto_le_app. Qed.
+  Proof. rewrite /lty_le lsty_le_eq.
+         iIntros "#H1 #H2 !>". by iApply iProto_le_app. Qed.
 
   Lemma lty_le_app_id_l S : âŠ¢ (END <++> S) <:> S.
-  Proof. rewrite /lty_app left_id. iSplit; by iModIntro. Qed.
+  Proof. rewrite /lty_app left_id.
+         iSplit; rewrite /lty_le lsty_le_eq /lsty_le_def; by iModIntro. Qed.
   Lemma lty_le_app_id_r S : âŠ¢ (S <++> END) <:> S.
-  Proof. rewrite /lty_app right_id. iSplit; by iModIntro. Qed.
+  Proof. rewrite /lty_app right_id.
+         iSplit; rewrite /lty_le lsty_le_eq /lsty_le_def; by iModIntro. Qed.
   Lemma lty_le_app_assoc S1 S2 S3 :
     âŠ¢ (S1 <++> S2) <++> S3 <:> S1 <++> (S2 <++> S3).
-  Proof. rewrite /lty_app assoc. iSplit; by iModIntro. Qed.
+  Proof. rewrite /lty_app assoc.
+         iSplit; rewrite /lty_le lsty_le_eq /lsty_le_def; by iModIntro. Qed.
 
   Lemma lty_le_app_send A S1 S2 : âŠ¢ (<!!> TY A; S1) <++> S2 <:> (<!!> TY A; S1 <++> S2).
   Proof.
-    rewrite /lty_app iProto_app_message iMsg_app_exist.
-    setoid_rewrite iMsg_app_base. iSplit; by iIntros "!> /=".
+    rewrite /lty_app iProto_app_message iMsg_app_exist. setoid_rewrite iMsg_app_base.
+    iSplit; rewrite /lty_le lsty_le_eq /lsty_le_def; by iIntros "!> /=".
   Qed.
   Lemma lty_le_app_recv A S1 S2 : âŠ¢ (<??> TY A; S1) <++> S2 <:> (<??> TY A; S1 <++> S2).
   Proof.
-    rewrite /lty_app iProto_app_message iMsg_app_exist.
-    setoid_rewrite iMsg_app_base. iSplit; by iIntros "!> /=".
+    rewrite /lty_app iProto_app_message iMsg_app_exist. setoid_rewrite iMsg_app_base.
+    iSplit; rewrite /lty_le lsty_le_eq /lsty_le_def; by iIntros "!> /=".
   Qed.
 
   Lemma lty_le_app_choice a (Ss : gmap Z (lsty Î£)) S2 :
@@ -423,8 +450,8 @@ Section subtyping_rules.
     rewrite /lty_app /lty_choice iProto_app_message iMsg_app_exist;
       setoid_rewrite iMsg_app_base; setoid_rewrite lookup_total_alt;
       setoid_rewrite lookup_fmap; setoid_rewrite fmap_is_Some.
-    iSplit; iIntros "!> /="; destruct a; iIntros (x); iExists x;
-      iMod 1 as %[S ->]; iSplitR; eauto.
+    iSplit; rewrite /lty_le lsty_le_eq; iIntros "!> /="; destruct a;
+      iIntros (x); iExists x; iMod 1 as %[S ->]; iSplitR; eauto.
   Qed.
   Lemma lty_le_app_select A Ss S2 :
     âŠ¢ lty_select Ss <++> S2 <:> lty_select ((.<++> S2) <$> Ss)%lty.
@@ -434,11 +461,13 @@ Section subtyping_rules.
   Proof. apply lty_le_app_choice. Qed.
 
   Lemma lty_le_dual S1 S2 : S2 <: S1 -âˆ— lty_dual S1 <: lty_dual S2.
-  Proof. iIntros "#H !>". by iApply iProto_le_dual. Qed.
+  Proof. rewrite /lty_le lsty_le_eq. iIntros "#H !>". by iApply iProto_le_dual. Qed.
   Lemma lty_le_dual_l S1 S2 : lty_dual S2 <: S1 -âˆ— lty_dual S1 <: S2.
-  Proof. iIntros "#H !>". by iApply iProto_le_dual_l. Qed.
+  Proof. rewrite /lty_le lsty_le_eq. iIntros "#H !>".
+         by iApply iProto_le_dual_l. Qed.
   Lemma lty_le_dual_r S1 S2 : S2 <: lty_dual S1 -âˆ— S1 <: lty_dual S2.
-  Proof. iIntros "#H !>". by iApply iProto_le_dual_r. Qed.
+  Proof. rewrite /lty_le lsty_le_eq. iIntros "#H !>".
+           by iApply iProto_le_dual_r. Qed.
 
   Lemma lty_le_dual_end : âŠ¢ lty_dual (Î£:=Î£) END <:> END.
   Proof. rewrite /lty_dual iProto_dual_end=> /=. apply lty_bi_le_refl. Qed.
@@ -447,7 +476,8 @@ Section subtyping_rules.
     âŠ¢ lty_dual (lty_message a (TY A; S)) <:> lty_message (action_dual a) (TY A; (lty_dual S)).
   Proof.
     rewrite /lty_dual iProto_dual_message iMsg_dual_exist.
-    setoid_rewrite iMsg_dual_base. iSplit; by iIntros "!> /=".
+    setoid_rewrite iMsg_dual_base.
+    iSplit; rewrite /lty_le lsty_le_eq /lsty_le_def; by iIntros "!> /=".
   Qed.
   Lemma lty_le_dual_send A S : âŠ¢ lty_dual (<!!> TY A; S) <:> (<??> TY A; lty_dual S).
   Proof. apply lty_le_dual_message. Qed.
@@ -460,8 +490,8 @@ Section subtyping_rules.
     rewrite /lty_dual /lty_choice iProto_dual_message iMsg_dual_exist;
       setoid_rewrite iMsg_dual_base; setoid_rewrite lookup_total_alt;
       setoid_rewrite lookup_fmap; setoid_rewrite fmap_is_Some.
-    iSplit; iIntros "!> /="; destruct a; iIntros (x); iExists x;
-      iMod 1 as %[S ->]; iSplitR; eauto.
+    iSplit; rewrite /lty_le lsty_le_eq; iIntros "!> /="; destruct a;
+      iIntros (x); iExists x; iMod 1 as %[S ->]; iSplitR; eauto.
   Qed.
 
   Lemma lty_le_dual_select (Ss : gmap Z (lsty Î£)) :
@@ -472,3 +502,4 @@ Section subtyping_rules.
   Proof. iApply lty_le_dual_choice. Qed.
 
 End subtyping_rules.
+