diff --git a/theories/logrel/copying.v b/theories/logrel/copying.v
index a7655fd7152f0a9e8ad55cc49ba618d5b82349c9..83e0e18dd6bcdd1a79cb5325de307f55069a68cc 100644
--- a/theories/logrel/copying.v
+++ b/theories/logrel/copying.v
@@ -23,11 +23,21 @@ Section copying.
     ⊢ copy A <: A.
   Proof. by iIntros (v) "!> #H". Qed.
 
+  Lemma coreP_desired_lemma (P : iProp Σ) :
+    □ (P -∗ □ P) -∗ coreP P -∗ P.
+  Proof.
+    iIntros "HP Hcore".
+  Admitted.
+
   Lemma lty_le_copy_minus A :
     copyable A -∗ copy- A <: A.
   Proof.
     iIntros "#HA". iIntros (v) "!> #Hv".
-  Admitted.
+    iSpecialize ("HA" $! v).
+    iApply coreP_desired_lemma.
+    - iModIntro. iApply "HA".
+    - iApply "Hv".
+  Qed.
 
   (* Copyability of types *)
   Lemma lty_unit_copyable :