diff --git a/theories/logrel/subtyping.v b/theories/logrel/subtyping.v
index 8cfbb16e0fc5b74e6defe151539b94e0fb3b4cf5..378f15ed7f12aedc7170ce7c6413f809fd9bb43a 100644
--- a/theories/logrel/subtyping.v
+++ b/theories/logrel/subtyping.v
@@ -323,43 +323,43 @@ Section subtype.
       iSplit; iIntros "!>".
       + rewrite /lsty_select /lsty_choice.
         iApply iProto_le_send.
-        iIntros "!>" (x) "%". iExists _ => /=.
+        iIntros "!>" (x HSs). iExists _ => /=.
         iSplit; first done.
         iSplit.
-        * rewrite lookup_fmap in a. rewrite ->fmap_is_Some in a. done.
-        * destruct a as [S HSs]=> /=.
-          rewrite lookup_total_alt lookup_total_alt HSs /=.
+        * rewrite lookup_fmap in HSs. rewrite ->fmap_is_Some in HSs. done.
+        * destruct HSs as [S HSs]=> /=.
+          rewrite !lookup_total_alt HSs /=.
           rewrite lookup_fmap in HSs.
           apply fmap_Some_1 in HSs as [S' [-> ->]].
           iApply iProto_le_refl.
       + rewrite /lsty_select /lsty_choice.
         iApply iProto_le_send.
-        iIntros "!>" (x) "%".
+        iIntros "!>" (x HSs).
         iExists _.
         iSplit; first done. iSplit.
         * by rewrite lookup_fmap fmap_is_Some.
-        * destruct a as [S HSs]=> /=.
-          rewrite lookup_total_alt lookup_total_alt lookup_fmap HSs.
+        * destruct HSs as [S HSs]=> /=.
+          rewrite !lookup_total_alt lookup_fmap HSs.
           iApply iProto_le_refl.
     - rewrite /lsty_app iProto_app_message_tele.
       iSplit; iIntros "!>".
       + rewrite /lsty_select /lsty_choice.
         iApply iProto_le_recv.
-        iIntros "!>" (x) "%". iExists _ => /=.
+        iIntros "!>" (x HSs). iExists _ => /=.
         iSplit; first done.
         iSplit.
         * by rewrite lookup_fmap fmap_is_Some.
-        * destruct a as [S HSs]=> /=.
-          rewrite lookup_total_alt lookup_total_alt lookup_fmap HSs.
+        * destruct HSs as [S HSs]=> /=.
+          rewrite !lookup_total_alt lookup_fmap HSs.
           iApply iProto_le_refl.
       + rewrite /lsty_select /lsty_choice.
         iApply iProto_le_recv.
-        iIntros "!>" (x) "%".
+        iIntros "!>" (x HSs).
         iExists _.
         iSplit; first done. iSplit.
-        * rewrite lookup_fmap in a. rewrite ->fmap_is_Some in a. done.
-        * destruct a as [S HSs]=> /=.
-          rewrite lookup_total_alt lookup_total_alt HSs /=.
+        * rewrite lookup_fmap in HSs. rewrite ->fmap_is_Some in HSs. done.
+        * destruct HSs as [S HSs]=> /=.
+          rewrite !lookup_total_alt HSs /=.
           rewrite lookup_fmap in HSs.
           apply fmap_Some_1 in HSs as [S' [-> ->]].
           iApply iProto_le_refl.
@@ -406,21 +406,21 @@ Section subtype.
       iSplit; iIntros "!>".
       + rewrite /lsty_select /lsty_choice.
         iApply iProto_le_recv.
-        iIntros "!>" (x) "%". iExists _ => /=.
+        iIntros "!>" (x HSs). iExists _ => /=.
         iSplit; first done.
         iSplit.
         * by rewrite lookup_fmap fmap_is_Some.
-        * destruct a as [S HSs]=> /=.
-          rewrite lookup_total_alt lookup_total_alt lookup_fmap HSs.
+        * destruct HSs as [S HSs]=> /=.
+          rewrite !lookup_total_alt lookup_fmap HSs.
           iApply iProto_le_refl.
       + rewrite /lsty_select /lsty_choice.
         iApply iProto_le_recv.
-        iIntros "!>" (x) "%".
+        iIntros "!>" (x HSs).
         iExists _.
         iSplit; first done. iSplit.
-        * rewrite lookup_fmap in a. rewrite ->fmap_is_Some in a. done.
-        * destruct a as [S HSs]=> /=.
-          rewrite lookup_total_alt lookup_total_alt HSs /=.
+        * rewrite lookup_fmap in HSs. rewrite ->fmap_is_Some in HSs. done.
+        * destruct HSs as [S HSs]=> /=.
+          rewrite !lookup_total_alt HSs /=.
           rewrite lookup_fmap in HSs.
           apply fmap_Some_1 in HSs as [S' [-> ->]].
           iApply iProto_le_refl.
@@ -428,23 +428,23 @@ Section subtype.
       iSplit; iIntros "!>".
       + rewrite /lsty_select /lsty_choice.
         iApply iProto_le_send.
-        iIntros "!>" (x) "%". iExists _ => /=.
+        iIntros "!>" (x HSs). iExists _ => /=.
         iSplit; first done.
         iSplit.
-      * rewrite lookup_fmap in a. rewrite ->fmap_is_Some in a. done.
-      * destruct a as [S HSs]=> /=.
-        rewrite lookup_total_alt lookup_total_alt HSs /=.
+      * rewrite lookup_fmap in HSs. rewrite ->fmap_is_Some in HSs. done.
+      * destruct HSs as [S HSs]=> /=.
+        rewrite !lookup_total_alt HSs /=.
         rewrite lookup_fmap in HSs.
         apply fmap_Some_1 in HSs as [S' [-> ->]].
         iApply iProto_le_refl.
       + rewrite /lsty_select /lsty_choice.
         iApply iProto_le_send.
-        iIntros "!>" (x) "%".
+        iIntros "!>" (x HSs).
         iExists _.
         iSplit; first done. iSplit.
         * by rewrite lookup_fmap fmap_is_Some.
-        * destruct a as [S HSs]=> /=.
-          rewrite lookup_total_alt lookup_total_alt lookup_fmap HSs.
+        * destruct HSs as [S HSs]=> /=.
+          rewrite !lookup_total_alt lookup_fmap HSs.
           iApply iProto_le_refl.
   Qed.