diff --git a/theories/logrel/ltyping.v b/theories/logrel/ltyping.v
index 2f00fdc3437a2df742a4f59036ac9607ac8593d2..a38fc2216f6ad16ebc6abe2cfcd4f83bfb5e2630 100755
--- a/theories/logrel/ltyping.v
+++ b/theories/logrel/ltyping.v
@@ -52,10 +52,6 @@ Class LTyUnOp {Σ} (op : un_op) (A B : lty Σ) :=
 Class LTyBinOp {Σ} (op : bin_op) (A1 A2 B : lty Σ) :=
   lty_bin_op v1 v2 : A1 v1 -∗ A2 v2 -∗ ∃ w, ⌜ bin_op_eval op v1 v2 = Some w ⌝ ∗ B w.
 
-(* Copy types *)
-Class LTyCopy `{invG Σ} (A : lty Σ) :=
-  lty_copy_pers v :> Persistent (A v).
-
 Section Environment.
   Context `{invG Σ}.
   Implicit Types A : lty Σ.
@@ -131,19 +127,20 @@ Section Environment.
     by iApply env_split_comm.
   Qed.
 
-  (* TODO: Get rid of side condition that x does not appear in Γ *)
-  Lemma env_split_copy Γ Γ1 Γ2 (x : string) A:
-    Γ !! x = None →
-    LTyCopy A →
-    env_split Γ Γ1 Γ2 -∗
-    env_split (<[x:=A]> Γ) (<[x:=A]> Γ1) (<[x:=A]> Γ2).
-  Proof.
-    iIntros (Hcopy HΓx) "#Hsplit". iIntros (vs) "!> HΓ".
-    iPoseProof (big_sepM_insert with "HΓ") as "[Hv HΓ]"; first by assumption.
-    iDestruct "Hv" as (v ?) "#HAv".
-    iDestruct ("Hsplit" with "HΓ") as "[HΓ1 HΓ2]".
-    iSplitL "HΓ1"; iApply big_sepM_insert_2; simpl; eauto.
-  Qed.
+  (* FIXME: copy *)
+  (* (* TODO: Get rid of side condition that x does not appear in Γ *) *)
+  (* Lemma env_split_copy Γ Γ1 Γ2 (x : string) A: *)
+  (*   Γ !! x = None → *)
+  (*   LTyCopy A → *)
+  (*   env_split Γ Γ1 Γ2 -∗ *)
+  (*   env_split (<[x:=A]> Γ) (<[x:=A]> Γ1) (<[x:=A]> Γ2). *)
+  (* Proof. *)
+  (*   iIntros (Hcopy HΓx) "#Hsplit". iIntros (vs) "!> HΓ". *)
+  (*   iPoseProof (big_sepM_insert with "HΓ") as "[Hv HΓ]"; first by assumption. *)
+  (*   iDestruct "Hv" as (v ?) "#HAv". *)
+  (*   iDestruct ("Hsplit" with "HΓ") as "[HΓ1 HΓ2]". *)
+  (*   iSplitL "HΓ1"; iApply big_sepM_insert_2; simpl; eauto. *)
+  (* Qed. *)
 
   (* TODO: Prove lemmas about this *)
   Definition env_copy (Γ Γ' : gmap string (lty Σ)) : iProp Σ :=
@@ -162,19 +159,20 @@ Section Environment.
     iApply ("Hcopy" with "Hvs").
   Qed.
 
-  Lemma env_copy_extend_copy x A Γ Γ' :
-    Γ !! x = None →
-    Γ' !! x = None →
-    LTyCopy A →
-    env_copy Γ Γ' -∗
-    env_copy (<[x:=A]> Γ) (<[x:=A]> Γ').
-  Proof.
-    iIntros (HΓx HΓ'x HcopyA) "#Hcopy". iIntros (vs) "!> Hvs". rewrite /env_ltyped.
-    iDestruct (big_sepM_insert with "Hvs") as "[HA Hvs]"; first done.
-    iDestruct ("Hcopy" with "Hvs") as "#Hvs'".
-    iDestruct "HA" as (v ?) "#HA".
-    iIntros "!>". iApply big_sepM_insert; first done. iSplitL; eauto.
-  Qed.
+  (* FIXME: copy *)
+  (* Lemma env_copy_extend_copy x A Γ Γ' : *)
+  (*   Γ !! x = None → *)
+  (*   Γ' !! x = None → *)
+  (*   LTyCopy A → *)
+  (*   env_copy Γ Γ' -∗ *)
+  (*   env_copy (<[x:=A]> Γ) (<[x:=A]> Γ'). *)
+  (* Proof. *)
+  (*   iIntros (HΓx HΓ'x HcopyA) "#Hcopy". iIntros (vs) "!> Hvs". rewrite /env_ltyped. *)
+  (*   iDestruct (big_sepM_insert with "Hvs") as "[HA Hvs]"; first done. *)
+  (*   iDestruct ("Hcopy" with "Hvs") as "#Hvs'". *)
+  (*   iDestruct "HA" as (v ?) "#HA". *)
+  (*   iIntros "!>". iApply big_sepM_insert; first done. iSplitL; eauto. *)
+  (* Qed. *)
 End Environment.
 
 (* The semantic typing judgement *)
diff --git a/theories/logrel/subtyping.v b/theories/logrel/subtyping.v
index c52b34ba1ee634fdd194ebe9c67f8e53c5fa717d..06b6e83ac35055e1c7fe01b927c68178f2e28831 100644
--- a/theories/logrel/subtyping.v
+++ b/theories/logrel/subtyping.v
@@ -40,9 +40,6 @@ Section subtype.
   Lemma lty_le_copy A : ⊢ copy A <: A.
   Proof. by iIntros (v) "!> #H". Qed.
 
-  Lemma lty_le_copyable A `{LTyCopy Σ A} : ⊢ A <: copy A.
-  Proof. by iIntros (v) "!> #H". Qed.
-
   Lemma lty_le_arr A11 A12 A21 A22 :
     ▷ (A21 <: A11) -∗ ▷ (A12 <: A22) -∗
     (A11 ⊸ A12) <: (A21 ⊸ A22).
diff --git a/theories/logrel/types.v b/theories/logrel/types.v
index ea7bb6e2a5d29874581edd7bf4b96f67ec77610d..8b0ef80d156d3b8141ce4c4bae5256d341de3e11 100644
--- a/theories/logrel/types.v
+++ b/theories/logrel/types.v
@@ -89,16 +89,10 @@ Section properties.
   (** Basic properties *)
   Global Instance lty_unit_unboxed : @LTyUnboxed Σ ().
   Proof. by iIntros (v ->). Qed.
-  Global Instance lty_unit_copy : @LTyCopy Σ _ ().
-  Proof. iIntros (v). apply _. Qed.
   Global Instance lty_bool_unboxed : @LTyUnboxed Σ lty_bool.
   Proof. iIntros (v). by iDestruct 1 as (b) "->". Qed.
-  Global Instance lty_bool_copy : @LTyCopy Σ _ lty_bool.
-  Proof. iIntros (v). apply _. Qed.
   Global Instance lty_int_unboxed : @LTyUnboxed Σ lty_int.
   Proof. iIntros (v). by iDestruct 1 as (i) "->". Qed.
-  Global Instance lty_int_copy : @LTyCopy Σ _ lty_int.
-  Proof. iIntros (v). apply _. Qed.
 
   Lemma ltyped_unit Γ : ⊢ Γ ⊨ #() : ().
   Proof. iIntros "!>" (vs) "_ /=". by iApply wp_value. Qed.
@@ -155,9 +149,6 @@ Section properties.
   Global Instance lty_copy_ne : NonExpansive (@lty_copy Σ).
   Proof. solve_proper. Qed.
 
-  Global Instance lty_copy_copy A : LTyCopy (copy A).
-  Proof. iIntros (v). apply _. Qed.
-
   (** Arrow properties *)
   Global Instance lty_arr_contractive n :
     Proper (dist_later n ==> dist_later n ==> dist n) lty_arr.
@@ -279,8 +270,6 @@ Section properties.
   Qed.
 
   (** Product properties  *)
-  Global Instance lty_prod_copy `{!LTyCopy A1, !LTyCopy A2} : LTyCopy (A1 * A2).
-  Proof. iIntros (v). apply _. Qed.
   Global Instance lty_prod_contractive n:
     Proper (dist_later n ==> dist_later n ==> dist n) (@lty_prod Σ).
   Proof. solve_contractive. Qed.
@@ -315,8 +304,6 @@ Section properties.
   Qed.
 
   (** Sum Properties *)
-  Global Instance lty_sum_copy `{!LTyCopy A1, !LTyCopy A2} : LTyCopy (A1 + A2).
-  Proof. iIntros (v). apply _. Qed.
   Global Instance lty_sum_contractive n :
     Proper (dist_later n ==> dist_later n ==> dist n) (@lty_sum Σ).
   Proof. solve_contractive. Qed.
@@ -412,10 +399,6 @@ Section properties.
   Qed.
 
   (** Existential properties *)
-  Global Instance lty_exist_copy C (Hcopy : ∀ A, LTyCopy (C A)) :
-    (LTyCopy (lty_exist C)).
-  Proof. intros v. apply bi.exist_persistent. intros A.
-         apply bi.later_persistent. apply Hcopy. Qed.
   Global Instance lty_exist_ne n :
     Proper (pointwise_relation _ (dist n) ==> dist n) (@lty_exist Σ).
   Proof. solve_proper. Qed.
@@ -423,10 +406,6 @@ Section properties.
     Proper (pointwise_relation _ (dist_later n) ==> dist n) (@lty_exist Σ).
   Proof. solve_contractive. Qed.
 
-  Global Instance lty_exist_lsty_copy C (Hcopy : ∀ A, LTyCopy (C A)) :
-    (LTyCopy (lty_exist_lsty C)).
-  Proof. intros v. apply bi.exist_persistent. intros A.
-         apply bi.later_persistent. apply Hcopy. Qed.
   Global Instance lty_exist_lsty_ne n :
     Proper (pointwise_relation _ (dist n) ==> dist n) (@lty_exist_lsty Σ).
   Proof. solve_proper. Qed.
@@ -513,18 +492,19 @@ Section properties.
     by iModIntro.
   Qed.
 
-  Lemma ltyped_load_copy A {copyA : LTyCopy A} :
-    ⊢ ∅ ⊨ load : ref_mut A → A * ref_mut A.
-  Proof.
-    iIntros (vs) "!> HΓ /=".
-    iApply wp_value.
-    iIntros "!>" (v) "Hv". rewrite /load. wp_pures.
-    iDestruct "Hv" as (l w ->) "[Hl #Hw]".
-    wp_load. wp_pures.
-    iExists w, #l. iSplit=> //. iFrame "Hw".
-    iExists l, w. iSplit=> //. iFrame "Hl".
-    by iModIntro.
-  Qed.
+  (* FIXME: copy *)
+  (* Lemma ltyped_load_copy A {copyA : LTyCopy A} : *)
+  (*   ⊢ ∅ ⊨ load : ref_mut A → A * ref_mut A. *)
+  (* Proof. *)
+  (*   iIntros (vs) "!> HΓ /=". *)
+  (*   iApply wp_value. *)
+  (*   iIntros "!>" (v) "Hv". rewrite /load. wp_pures. *)
+  (*   iDestruct "Hv" as (l w ->) "[Hl #Hw]". *)
+  (*   wp_load. wp_pures. *)
+  (*   iExists w, #l. iSplit=> //. iFrame "Hw". *)
+  (*   iExists l, w. iSplit=> //. iFrame "Hl". *)
+  (*   by iModIntro. *)
+  (* Qed. *)
 
   Definition store : val := λ: "r" "new", "r" <- "new";; "r".
 
@@ -545,8 +525,6 @@ Section properties.
   Proof. solve_proper. Qed.
   Global Instance lty_ref_shr_unboxed A : LTyUnboxed (ref_shr A).
   Proof. iIntros (v). by iDestruct 1 as (l ->) "?". Qed.
-  Global Instance lty_ref_shr_copy A : LTyCopy (ref_shr A).
-  Proof. iIntros (v). apply _. Qed.
 
   Definition fetch_and_add : val := λ: "r" "inc", FAA "r" "inc".
   Lemma ltyped_fetch_and_add :
@@ -565,26 +543,27 @@ Section properties.
     by iExists m.
   Qed.
 
-  Lemma ltyped_ref_shr_load (A : lty Σ) {copyA : LTyCopy A} :
-    ⊢ ∅ ⊨ load : ref_shr A → (A * ref_shr A).
-  Proof.
-    iIntros (vs) "!> _ /=". iApply wp_value. iIntros "!>" (r) "Hr".
-    iApply wp_fupd. rewrite /load; wp_pures.
-    iDestruct "Hr" as (l ->) "Hr".
-    iMod (fupd_mask_mono with "Hr") as "#Hr"; first done.
-    wp_bind (!#l)%E.
-    iInv (ref_shrN .@ l) as (v) "[>Hl #HA]" "Hclose".
-    wp_load.
-    iMod ("Hclose" with "[Hl HA]") as "_".
-    { iExists v. iFrame "Hl HA". }
-    iIntros "!>". wp_pures. iIntros "!>".
-    iExists _, _.
-    iSplit; first done.
-    iFrame "HA".
-    iExists _.
-    iSplit; first done.
-    by iFrame "Hr".
-  Qed.
+  (* FIXME: copy *)
+  (* Lemma ltyped_ref_shr_load (A : lty Σ) {copyA : LTyCopy A} : *)
+  (*   ⊢ ∅ ⊨ load : ref_shr A → (A * ref_shr A). *)
+  (* Proof. *)
+  (*   iIntros (vs) "!> _ /=". iApply wp_value. iIntros "!>" (r) "Hr". *)
+  (*   iApply wp_fupd. rewrite /load; wp_pures. *)
+  (*   iDestruct "Hr" as (l ->) "Hr". *)
+  (*   iMod (fupd_mask_mono with "Hr") as "#Hr"; first done. *)
+  (*   wp_bind (!#l)%E. *)
+  (*   iInv (ref_shrN .@ l) as (v) "[>Hl #HA]" "Hclose". *)
+  (*   wp_load. *)
+  (*   iMod ("Hclose" with "[Hl HA]") as "_". *)
+  (*   { iExists v. iFrame "Hl HA". } *)
+  (*   iIntros "!>". wp_pures. iIntros "!>". *)
+  (*   iExists _, _. *)
+  (*   iSplit; first done. *)
+  (*   iFrame "HA". *)
+  (*   iExists _. *)
+  (*   iSplit; first done. *)
+  (*   by iFrame "Hr". *)
+  (* Qed. *)
 
   Lemma ltyped_ref_shrstore (A : lty Σ) :
     ⊢ ∅ ⊨ store : ref_shr A → A → ref_shr A.