Clean up

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.