diff --git a/theories/examples/subprotocols.v b/theories/examples/subprotocols.v
index 3ea323eb44fa2473e35f3b6a13d8fae4ee74c719..75f1d6de44a40c31314fef89699b7a5f8a1cf2d7 100644
--- a/theories/examples/subprotocols.v
+++ b/theories/examples/subprotocols.v
@@ -7,9 +7,6 @@ Section basics.
     l2' ↦ #22 -∗
     (<! (l1 l2 : loc)> MSG (#l1, #l2) {{ l1 ↦ #20 ∗ l2 ↦ #22 }}; END)%proto ⊑
       (<! (l1 : loc)> MSG (#l1, #l2') {{ l1 ↦ #20 }}; END)%proto.
-  Proof.
-    iIntros "Hl2'" (l1) "Hl1". iExists l1, l2'.
-    iSplitL; eauto with iFrame.
-  Qed.
+  Proof. iIntros "Hl2'" (l1) "Hl1". iExists l1, l2'. by iFrame. Qed.
 
 End pair.