diff --git a/theories/logrel/subtyping.v b/theories/logrel/subtyping.v
index 9fe1c1c09c5ede50bbb213c24451cf7f4e5f28af..6b6df0d1f99158f7be33e0cd527958fe660c0c3d 100644
--- a/theories/logrel/subtyping.v
+++ b/theories/logrel/subtyping.v
@@ -242,7 +242,7 @@ Section subtype.
     Ps2 ⊆ Ps1 →
     ⊢ lsty_select Ps1 <p: lsty_select Ps2.
   Proof.
-    iIntros (Hnone) "!>".
+    iIntros (Hsub) "!>".
     iApply iProto_le_send.
     iIntros (x) ">% !>"=> /=.
     iExists _. iSplit=> //.
@@ -279,7 +279,7 @@ Section subtype.
     Ps1 ⊆ Ps2 →
     ⊢ lsty_branch Ps1 <p: lsty_branch Ps2.
   Proof.
-    iIntros (Hnone) "!>".
+    iIntros (Hsub) "!>".
     iApply iProto_le_recv.
     iIntros (x) ">% !>"=> /=.
     iExists _. iSplit=> //.