diff --git a/theories/logrel/subtyping_rules.v b/theories/logrel/subtyping_rules.v
index 6c6a27b9535aa60edc6b7a997f9139f02409ebc3..31beeb3494732d84d6c74ac7a97d236465cf9762 100644
--- a/theories/logrel/subtyping_rules.v
+++ b/theories/logrel/subtyping_rules.v
@@ -298,7 +298,7 @@ Section subtyping_rules.
     iApply iProto_le_trans;
       [iApply iProto_le_base; iApply (iProto_le_exist_intro_l _ x2)|]; simpl.
     iApply iProto_le_payload_elim_r.
-    iMod 1 as "%". revert H1.
+    iMod 1 as %HSs. revert HSs.
     rewrite !lookup_total_alt !lookup_fmap fmap_is_Some; iIntros ([S ->]) "/=".
     iApply iProto_le_trans; [iApply iProto_le_base_swap|]. iSplitL; [by eauto|].
     iModIntro. by iExists v1.