diff --git a/theories/examples/refinements/memoization.v b/theories/examples/refinements/memoization.v
index fd28c0559e734545146704c004958e2e44aa9123..d2d520fb5b5239bcbc95ac1871a6184bfd507ed7 100644
--- a/theories/examples/refinements/memoization.v
+++ b/theories/examples/refinements/memoization.v
@@ -850,6 +850,22 @@ Section fibonacci.
     - iModIntro. iIntros (e v Hexec K).
       iApply exec_src_update. apply exec_frame, Hexec.
   Qed.
+
+
+  Corollary fib_deep_memoized_instantiate (n: nat) K:
+    src (fill K (fib #n)) ⊢ SEQ (mem_rec eq_heaplang fib_template #n) ⟨⟨ w, ∃ (m: nat), ⌜w = #m⌝ ∗ src (fill K (Val #m)) ⟩⟩.
+  Proof.
+    iStartProof. iIntros "Hsrc Hna".
+    wp_bind (mem_rec eq_heaplang fib_template).
+    iApply (rwp_wand with "[Hna]").
+    { iApply fib_deep_memoized. iFrame. }
+    iIntros (f) "[Hna Himpl]". rewrite /implements.
+    iSpecialize ("Himpl" $! #n #n K with "[] Hsrc Hna").
+    { iExists _; done. }
+    iApply (rwp_wand with "Himpl").
+    iIntros (v) "($&H)". iDestruct "H" as (w) "(Hrel & Hsrc & _)".
+    iDestruct "Hrel" as %[? [-> ->]]. iExists _. by iFrame.
+  Qed.
 End fibonacci.
 
 Section levenshtein.