diff --git a/theories/logrel/copying.v b/theories/logrel/copying.v
index 79bc1a6d4603ac88554ea4b6164e231669496f68..a7655fd7152f0a9e8ad55cc49ba618d5b82349c9 100644
--- a/theories/logrel/copying.v
+++ b/theories/logrel/copying.v
@@ -96,15 +96,21 @@ Section copying.
 
   (* Copyability of recursive types *)
   Lemma lty_rec_copy C `{!Contractive C} :
-    □ (∀ A, copyable A -∗ copyable (C A)) -∗ copyable (lty_rec C).
+    □ (∀ A, ▷ copyable A -∗ copyable (C A)) -∗ copyable (lty_rec C).
   Proof.
     iIntros "#Hcopy".
-    iLöb as "#IH".
+    iLöb as "IH".
     iIntros (v) "!> Hv".
-    rewrite /lty_rec {2}fixpoint_unfold.
-    (* iEval (rewrite fixpoint_unfold) *)
-    (* TODO: Rewriting goes crazy here *)
-  Admitted.
+    rewrite /lty_rec.
+    rewrite {2}fixpoint_unfold.
+    iSpecialize ("Hcopy" with "IH").
+    rewrite {3}/lty_rec_aux.
+    iSpecialize ("Hcopy" with "Hv").
+    iDestruct "Hcopy" as "#Hcopy".
+    iModIntro.
+    iEval (rewrite fixpoint_unfold).
+    iApply "Hcopy".
+  Qed.
 
   (* TODO: Get rid of side condition that x does not appear in Γ *)
   Lemma env_split_copy Γ Γ1 Γ2 (x : string) A: