diff --git a/theories/examples/subprotocols.v b/theories/examples/subprotocols.v
index d828053d1b4eac7c439cda594f95e890e71004ea..2a4d355d9a5d2dfb04b9fe214ad62c7f94814238 100644
--- a/theories/examples/subprotocols.v
+++ b/theories/examples/subprotocols.v
@@ -11,6 +11,14 @@ Section basics.
     (<! (l1 : loc)> MSG (#l1, #l2') {{ l1 ↦ #20 }}; END).
   Proof. iIntros "Hl2'" (l1) "Hl1". iExists l1, l2'. by iFrame "Hl1 Hl2'". Qed.
 
+  Lemma framing_example (P Q R : iProp Σ) (v w : val) :
+    ⊢ ((<!> MSG v {{ P }} ; <?> MSG w {{ Q }}; END)%proto ⊑
+       (<!> MSG v {{ P ∗ R }} ; <?> MSG w {{ Q ∗ R }};END)%proto)%proto.
+  Proof.
+    iIntros "[HP HR]". iFrame "HP". iModIntro.
+    iIntros "HQ". iFrame "HQ HR". eauto.
+  Qed.
+
   Section program_reuse.
     Context {T U R : Type}.
     Context (IT : T -> val -> iProp Σ).