diff --git a/theories/rust_typing/ltypes.v b/theories/rust_typing/ltypes.v
index d25eca4a4b18e7ae295e25931658ed4f6d6e8cba..a86d1a3f36d9cbd8334b0618e081e8976bf111f8 100644
--- a/theories/rust_typing/ltypes.v
+++ b/theories/rust_typing/ltypes.v
@@ -779,10 +779,10 @@ Section ltype_def.
         (lt_full : lty)
     | ShadowedLty {rt : Type} (lt_cur : lty) (r_cur : place_rfn rt) (lt_full : lty)
     | MagicLty
-        {rt_cur : Type}
-        (lt_cur : lty) (lt_full : lty)
-        (Cpre : rt_cur → iProp Σ)
-        (Cpost : rt_cur → iProp Σ)
+        {rt_inner rt_full : Type}
+        (lt_cur : lty) (lt_inner : lty) (lt_full : lty)
+        (Cpre : rt_inner → rt_full → iProp Σ)
+        (Cpost : rt_inner → rt_full → iProp Σ)
   .
 
   (*
@@ -816,8 +816,8 @@ Section ltype_def.
         lty_rt lt_full
     | ShadowedLty lt_cur r_cur lt_full =>
         lty_rt lt_full
-    | MagicLty _ lt_full _ _ =>
-        lty_rt lt_full
+    | MagicLty lt_cur _ _ _ _ =>
+        lty_rt lt_cur
     end.
 
   Fixpoint lty_st (lt : lty) : syn_type :=
@@ -838,8 +838,8 @@ Section ltype_def.
         lty_st lt_full
     | ShadowedLty lt_cur r_cur lt_full =>
         lty_st lt_full
-    | MagicLty _ lt_full _ _ =>
-        lty_st lt_full
+    | MagicLty lt_cur _ _ _ _ =>
+        lty_st lt_cur
     end.
 
   Fixpoint lty_wf (lt : lty) : Prop :=
@@ -865,8 +865,8 @@ Section ltype_def.
         lty_wf lt
     | @ShadowedLty rt_cur lt_cur r_cur lt_full =>
         lty_wf lt_cur ∧ lty_wf lt_full ∧ lty_rt lt_cur = rt_cur
-    | @MagicLty rt_cur lt_cur lt_full _ _ =>
-        rt_cur = lty_rt lt_cur ∧ lty_wf lt_cur ∧ lty_wf lt_full
+    | @MagicLty rt_inner rt_full lt_cur lt_inner lt_full _ _ =>
+        rt_inner = lty_rt lt_inner ∧ rt_full = lty_rt lt_full ∧ lty_wf lt_cur ∧ lty_wf lt_inner ∧ lty_wf lt_full
     end.
 
 
@@ -891,8 +891,9 @@ Section ltype_def.
           P lt_cur → P lt_inner → P lt_full → P (OpenedLty lt_cur lt_inner lt_full Cpre Cpost)) →
       (∀ κs (lt_full : lty), P lt_full → P (CoreableLty κs lt_full)) →
       (∀ (rt_cur : Type) (lt_cur : lty) (r_cur : place_rfn rt_cur) (lt_full : lty), P lt_cur → P lt_full → P (ShadowedLty lt_cur r_cur lt_full)) →
-      (∀ (rt_cur : Type) (lt_cur lt_full : lty) (Cpre Cpost : rt_cur → iProp Σ),
-        P lt_cur → P lt_full → P (MagicLty lt_cur lt_full Cpre Cpost)) →
+      (∀ (rt_inner rt_full : Type) (lt_cur lt_inner lt_full : lty)
+        (Cpre : rt_inner → rt_full → iProp Σ) (Cpost : rt_inner → rt_full → iProp Σ),
+          P lt_cur → P lt_inner → P lt_full → P (MagicLty lt_cur lt_inner lt_full Cpre Cpost)) →
       ∀ lt : lty, P lt.
   Proof.
     intros P Hblocked Hshrblocked Hofty Halias Hmut Hshr Hbox Hptr Hstruct Harr Henum Hopened Hcoreable Hshadow Hmagic.
@@ -919,7 +920,7 @@ Section ltype_def.
           _
       | ShadowedLty lt_cur r_cur lt_full =>
           _
-      | MagicLty _ _ _ _ =>
+      | MagicLty _ _ _ _ _ =>
           _
       end); [apply IH.. | | | | | | | ].
       - apply Hstruct.
@@ -951,8 +952,9 @@ Section ltype_def.
           P lt_cur → P lt_inner → P lt_full → P (OpenedLty lt_cur lt_inner lt_full Cpre Cpost)) →
       (∀ κs (lt_full : lty), P lt_full → P (CoreableLty κs lt_full)) →
       (∀ (rt_cur : Type) (lt_cur : lty) (r_cur : place_rfn rt_cur) (lt_full : lty), P lt_cur → P lt_full → P (ShadowedLty lt_cur r_cur lt_full)) →
-      (∀ (rt_cur : Type) (lt_cur lt_full : lty) (Cpre Cpost : rt_cur → iProp Σ),
-        P lt_cur → P lt_full → P (MagicLty lt_cur lt_full Cpre Cpost)) →
+      (∀ (rt_inner rt_full : Type) (lt_cur lt_inner lt_full : lty)
+        (Cpre : rt_inner → rt_full → iProp Σ) (Cpost : rt_inner → rt_full → iProp Σ),
+          P lt_cur → P lt_inner → P lt_full → P (MagicLty lt_cur lt_inner lt_full Cpre Cpost)) →
       ∀ lt : lty, P lt.
   Proof.
     intros P ? ? ? ? ? ? ? ? Hstruct Harr Henum Hopened Hcoreable Hshadow Hmagic lt.
@@ -995,8 +997,9 @@ Section ltype_def.
       (∀ κs (lt_full : lty), P lt_full → P (CoreableLty κs lt_full)) →
       (∀ (lt_cur : lty) (r_cur : place_rfn (lty_rt lt_cur)) (lt_full : lty),
         P lt_cur → P lt_full → P (ShadowedLty lt_cur r_cur lt_full)) →
-      (∀ (lt_cur lt_full : lty) (Cpre Cpost : lty_rt lt_cur → iProp Σ),
-        P lt_cur → P lt_full → P (MagicLty lt_cur lt_full Cpre Cpost)) →
+      (∀ (lt_cur lt_inner lt_full : lty) (Cpre : (lty_rt lt_inner) → lty_rt lt_full → iProp Σ)
+        (Cpost : (lty_rt lt_inner) → (lty_rt lt_full) → iProp Σ),
+          P lt_cur → P lt_inner → P lt_full → P (MagicLty lt_cur lt_inner lt_full Cpre Cpost)) →
       ∀ lt : lty, lty_wf lt → P lt.
   Proof.
     intros P ???????? Hstruct Harr Henum Hopened Hcoreable Hshadow Hmagic lt Hwf.
@@ -1018,7 +1021,7 @@ Section ltype_def.
     - eapply Hcoreable; eauto.
     - destruct Hwf as (? & ? & <-).
       eapply Hshadow; eauto.
-    - destruct Hwf as (-> & Hcur & Hfull).
+    - destruct Hwf as (Heq1 & Heq2 & Hcur & Hinner & Hfull ). subst.
       eapply Hmagic; eauto.
   Qed.
 
@@ -1042,8 +1045,8 @@ Section ltype_def.
         1 + lty_size lt_full
     | ShadowedLty lt_cur r_cur lt_full =>
         1 + lty_size lt_cur + lty_size lt_full
-    | MagicLty lt_cur lt_full Cpre Cpost =>
-        1 + max (lty_size lt_cur) (lty_size lt_full)
+    | MagicLty lt_cur lt_inner lt_full Cpre Cpost =>
+        1 + max (lty_size lt_cur) (max (lty_size lt_inner) (lty_size lt_full))
     end.
   Definition lty_size_rel : lty → lty → Prop :=
     ltof _ lty_size.
@@ -1089,8 +1092,8 @@ Section ltype_def.
         lty_core lt_full
     | ShadowedLty lt_cur r_cur lt_full =>
         lty_core lt_full
-    | MagicLty lt_cur lt_full Cpre Cpost =>
-        lty_core lt_full
+    | MagicLty lt_cur lt_inner lt_full Cpre Cpost =>
+        MagicLty lt_cur lt_inner lt_full Cpre Cpost
     end.
 
   Lemma lty_core_syn_type_eq (lt : lty) :
@@ -1117,7 +1120,7 @@ Section ltype_def.
   Lemma lty_core_wf lt :
     lty_wf lt → lty_wf (lty_core lt).
   Proof.
-    induction lt as [ | | | | | | | | lts IH sls | rt def len lts IH | rt en variant lte IH | | rt lt IH | | ] using lty_induction; simpl; [done.. | | | | done | | | ].
+    induction lt as [ | | | | | | | | lts IH sls | rt def len lts IH | rt en variant lte IH | | rt lt IH | | ] using lty_induction; simpl; [done.. | | | | done | | | done ].
     - rewrite -!Forall_Forall_cb.
       rewrite Forall_fmap.
       apply Forall_impl_strong.
@@ -1133,8 +1136,6 @@ Section ltype_def.
       rewrite lty_core_rt_eq. done.
     - done.
     - intros (? & ? & <-). eauto.
-    - intros (? & []).
-      by apply IHlt2.
   Qed.
 
   Lemma lty_size_core (lt : lty) :
@@ -1688,12 +1689,25 @@ Section ltype_def.
         ⌜lty_st lt_cur = lty_st lt_full⌝ ∗
         lty_own_pre core lt_cur k π ((rew Heq_cur in r_cur)) l ∗
         lty_own_pre core lt_full k π r l)%I;
-    lty_own_pre core (@MagicLty rt_cur lt_cur lt_full Cpre Cpost) k π r l :=
+    lty_own_pre core (@MagicLty rt_inner rt_full lt_cur lt_inner lt_full Cpre Cpost) k π r l :=
       (** MagicLty *)
-      match k with (* TODO: MagicType *)
-      | Owned wl => False
-      | Uniq κ γ => False
-      | Shared κ => False
+      ∃ ly, ⌜use_layout_alg (lty_st lt_cur) = Some ly⌝ ∗
+        ⌜l `has_layout_loc` ly⌝ ∗
+        loc_in_bounds l 0 (ly_size ly) ∗
+        ⌜lty_st lt_cur = lty_st lt_inner⌝ ∗
+        ⌜lty_st lt_inner = lty_st lt_full⌝ ∗
+
+      match k with
+      | Owned wl =>
+          lty_own_pre false lt_cur (Owned false) π r l ∗
+          logical_step lftE
+          (∃ (Heq_inner : rt_inner = lty_rt lt_inner) (Heq_full : rt_full = lty_rt lt_full),
+            ∀ (r : rt_inner) (r' : rt_full),
+              Cpre r r' -∗
+              lty_own_pre false lt_inner (Owned false) π (PlaceIn (rew [id] Heq_inner in r)) l ={lftE}=∗
+              lty_own_pre true lt_full (Owned wl) π (PlaceIn (rew [id] Heq_full in r')) l ∗
+              Cpost r r')
+      | _ => False
       end
   .
   Solve Obligations with first [unfold lty_size_rel, ltof; simpl; lia | intros; eauto using struct_lts_size_decreasing, array_lts_size_decreasing].
@@ -1765,8 +1779,9 @@ Section ltype_def.
     - iDestruct "Hown" as "(%ly & ? & ? & _)". eauto.
     - iDestruct ("Hown") as (->) "(%Hst & Ha & Hb)".
       simpl. rewrite -Hst. iApply ("IH" with "Ha").
-    - admit. (* TODO: MagicType *)
-  Admitted.
+    - simpl. iDestruct "Hown" as "(%ly & ? & ? & ? & ? & _)".
+      eauto.
+  Qed.
 
   Lemma lty_own_loc_in_bounds (lt : lty) k π r l ly :
     syn_type_has_layout (lty_st lt) ly →
@@ -1811,12 +1826,14 @@ Section ltype_def.
     - iDestruct "Hown" as (->) "(%Hst & Ha & Hb)".
       simpl in Ha. rewrite -Hst in Ha.
       iApply "IH"; done.
-    - admit. (* TODO: MagicType *)
-  Admitted.
+    - iDestruct "Hown" as "(%ly' & %Halg & ? & ? & ? & ? & _)".
+      simpl in *. assert (ly' = ly) as ->. { by eapply syn_type_has_layout_inj. }
+      iFrame.
+  Qed.
 
   Lemma lty_own_Owned_true_false (lt : lty) π r l :
     match lt with
-    | OpenedLty _ _ _ _ _ | CoreableLty _ _ | ShadowedLty _ _ _ | MagicLty _ _ _ _ => False
+    | OpenedLty _ _ _ _ _ | CoreableLty _ _ | ShadowedLty _ _ _ | MagicLty _ _ _ _ _ => False
     | _ => True
     end →
     lty_own lt (Owned true) π r l -∗
@@ -1844,7 +1861,7 @@ Section ltype_def.
   Qed.
   Lemma lty_own_Owned_false_true (lt : lty) π r l :
     match lt with
-    | OpenedLty _ _ _ _ _ | CoreableLty _ _ | ShadowedLty _ _ _ | MagicLty _ _ _ _ => False
+    | OpenedLty _ _ _ _ _ | CoreableLty _ _ | ShadowedLty _ _ _ | MagicLty _ _ _ _ _ => False
     | _ => True
     end →
     (lty_own lt (Owned false) π r l) -∗
@@ -1986,7 +2003,7 @@ Section ltype_def.
   Lemma lty_own_core_core (lt : lty) k π r r' Heq l :
     r' = (transport_rfn Heq r) →
     lty_own_pre true (lty_core lt) k π r l ≡ lty_own_pre true lt k π r' l.
-  Proof. (* TODO: MagicType *)
+  Proof.
     intros ->. rewrite /lty_own_core.
     induction lt as [ | | | | lt IH κ | lt IH κ | lt IH | lt ls IH | lts IH sls | rt def len lts IH | rt en variant lt IH | | | | ] using lty_induction in k, π, r, l, Heq |-*; simpl in *.
     - simp lty_own_pre. rewrite (UIP_refl _ _ Heq). done.
@@ -2120,8 +2137,8 @@ Section ltype_def.
     - simp lty_own_pre. rewrite (UIP_refl _ _ Heq). done.
     - simp lty_own_pre.
     - simp lty_own_pre.
-    - admit.
-  Admitted.
+    - simp lty_own_pre. rewrite (UIP_refl _ _ Heq). done.
+  Qed.
   Lemma lty_own_core_core' (lt : lty) k π r Heq l :
     lty_own_pre true (lty_core lt) k π r l ≡ lty_own_pre true lt k π (transport_rfn Heq r) l.
   Proof.
@@ -2197,7 +2214,7 @@ Section ltype_def.
 
  Lemma lty_own_core_equiv (lt : lty) core k π r l Heq :
     lty_own_pre true lt k π r l ≡ lty_own_pre core (lty_core lt) k π (transport_rfn Heq r) l.
-  Proof. (* TODO: MagicType *)
+  Proof.
     rewrite /lty_own_core /lty_own.
     induction lt as [ | | | | lt IH κ | lt IH κ | lt IH | lt ls IH | lts IH sls | def len lts IH IH' | rt en variant lt  IH | | | | ] using lty_induction in k, π, r, l, Heq, core |-*; simpl in *.
     - simp lty_own_pre. rewrite (UIP_refl _ _ Heq). done.
@@ -2329,8 +2346,8 @@ Section ltype_def.
     - rewrite (UIP_refl _ _ Heq). simp lty_own_pre. done.
     - simp lty_own_pre.
     - simp lty_own_pre.
-    - admit.
-  Admitted.
+    - rewrite (UIP_refl _ _ Heq). simp lty_own_pre. done.
+  Qed.
 
   Local Lemma place_rfn_interp_shared_transport_eq {rt rt'} (r : place_rfn rt) (r' : rt) (Heq : rt = rt') :
     place_rfn_interp_shared r r' -∗
@@ -2351,7 +2368,7 @@ Section ltype_def.
 
   Lemma lty_own_shared_to_core lt κ0 π r l Heq :
     lty_own lt (Shared κ0) π r l -∗ lty_own (lty_core lt) (Shared κ0) π (transport_rfn Heq r) l.
-  Proof. (* TODO: MagicType *)
+  Proof.
     rewrite /lty_own_core /lty_own.
     induction lt as [ | | | | lt IH κ | lt IH κ | lt IH | lt ls IH | lts IH sls | rt def len lts IH  | rt en variant lt IH | | | ???? IH1 IH2 | ] using lty_induction in κ0, π, r, l, Heq |-*; simpl in *.
     - simp lty_own_pre. iIntros "(% & _ & _ & _ & _ & [])".
@@ -2477,8 +2494,9 @@ Section ltype_def.
     - simp lty_own_pre.
       iIntros "(%Heq_cur & %Hst & Ha & Hb)".
       iApply (IH2 with "Hb").
-    - admit.
-  Admitted.
+    - simp lty_own_pre.
+      iIntros "(%ly & % & % & ? & % & % & [])".
+  Qed.
   (* NOTE: The reverse does not hold because the core of [BlockedLty] is [OfTy], which has a sharing predicate, but [BlockedLty] doesn't *)
 
   (** ** We define derived versions on top that expose the refinement type as an index.
@@ -2666,15 +2684,16 @@ Section ltype_def.
   Global Arguments ShadowedLtype : simpl never.
   Global Typeclasses Opaque ShadowedLtype.
 
-  Program Definition MagicLtype {rt_cur rt_full} (lt_cur : ltype rt_cur) (lt_full : ltype rt_full) (Cpre Cpost : rt_cur → iProp Σ) : ltype rt_full := {|
-    ltype_lty := MagicLty (ltype_lty lt_cur) (ltype_lty lt_full) Cpre Cpost;
+  Program Definition MagicLtype {rt_cur rt_inner rt_full} (lt_cur : ltype rt_cur) (lt_inner : ltype rt_inner) (lt_full : ltype rt_full)
+      (Cpre : rt_inner → rt_full → iProp Σ) (Cpost : rt_inner → rt_full → iProp Σ) : ltype rt_cur := {|
+    ltype_lty := MagicLty (ltype_lty lt_cur) (ltype_lty lt_inner) (ltype_lty lt_full) Cpre Cpost;
   |}.
   Next Obligation.
     intros rt_cur rt_full lt_cur lt_full Cpre Cpost. simpl.
     rewrite ltype_rt_agree. done.
   Qed.
   Next Obligation.
-    intros rt_cur rt_full [lt_cur <- Hcur] [lt_full <- Hfull] Cpre Cpost; simpl.
+    intros rt_cur rt_inner rt_full [lt_cur <- Hcur] [lt_inner <- Hinner] [lt_full <- Hfull] Cpre Cpost; simpl.
     eauto.
   Qed.
   Global Typeclasses Opaque MagicLtype.
@@ -2794,8 +2813,10 @@ Section ltype_def.
       (∀ (rt_full : Type) κs (lt_full : ltype rt_full), P _ lt_full → P _ (CoreableLtype κs lt_full)) →
       (∀ (rt_cur rt_full : Type) (lt_cur : ltype rt_cur) (r_cur : place_rfn rt_cur) (lt_full : ltype rt_full),
         P _ lt_cur → P _ lt_full → P _ (ShadowedLtype lt_cur r_cur lt_full)) →
-      (∀ (rt_cur rt_full : Type) (lt_cur : ltype rt_cur) (lt_full : ltype rt_full) (Cpre Cpost : rt_cur → iProp Σ),
-        P _ lt_cur → P _ lt_full → P _ (MagicLtype lt_cur lt_full Cpre Cpost)) →
+      (∀ (rt_cur rt_inner rt_full : Type) (lt_cur : ltype rt_cur) (lt_inner : ltype rt_inner) (lt_full : ltype rt_full)
+        (Cpre : rt_inner → rt_full → iProp Σ) (Cpost : rt_inner → rt_full → iProp Σ),
+        P _ lt_cur → P _ lt_inner → P _ lt_full →
+        P _ (MagicLtype lt_cur lt_inner lt_full Cpre Cpost)) →
       ∀ (rt : Type) (lt : ltype rt), P _ lt.
     Proof.
       intros Hblocked Hshrblocked Hofty Halias Hmut Hshr Hbox Hptr Hstruct Harr Hen Hopened Hcoreable Hshadow Hmagic.
@@ -2806,7 +2827,7 @@ Section ltype_def.
         intros Hwf1 Hwf2. rewrite (proof_irrelevance _ Hwf1 Hwf2). done. }
 
       intros rt [lt <- Hwf].
-      induction lt as [ | | | | lt IH κ | lt IH κ | lt IH | lt ls IH | lts IH sls | rt def len lts IH | rt en variant lte IH | rt_inner rt_full lt_cur lt_inner lt_full Cpre Cpost IH_cur IH_inner IH_full | κ lt_full IH | rt_cur lt_cur r_cur lt_full IH_cur IH_full | rt_full lt_cur lt_full Cpre Cpost IH_cur IH_full ] using lty_induction; simpl.
+      induction lt as [ | | | | lt IH κ | lt IH κ | lt IH | lt ls IH | lts IH sls | rt def len lts IH | rt en variant lte IH | rt_inner rt_full lt_cur lt_inner lt_full Cpre Cpost IH_cur IH_inner IH_full | κ lt_full IH | rt_cur lt_cur r_cur lt_full IH_cur IH_full | rt_inner rt_full lt_cur lt_inner lt_full Cpre Cpost IH_cur IH_inner IH_full ] using lty_induction; simpl.
       - eapply P_irrel. apply Hblocked.
       - eapply P_irrel. apply Hshrblocked.
       - eapply P_irrel. apply Hofty.
@@ -2851,8 +2872,8 @@ Section ltype_def.
       - destruct Hwf as (Hwf_cur & Hwf_full & <-).
         specialize (Hshadow _ _ _ r_cur _ (IH_cur Hwf_cur) (IH_full Hwf_full)).
         eapply P_irrel. eapply Hshadow.
-      - destruct Hwf as (Heq & Hwf_cur & Hwf_full); subst.
-        specialize (Hmagic _ _ _ _ Cpre Cpost (IH_cur Hwf_cur) (IH_full Hwf_full)).
+      - destruct Hwf as (Heq1 & Heq2 & Hwf_cur & Hwf_inner & Hwf_full); subst.
+        specialize (Hmagic _ _ _ _ _ _ Cpre Cpost (IH_cur Hwf_cur) (IH_inner Hwf_inner) (IH_full Hwf_full)).
         eapply P_irrel. eapply Hmagic.
     Qed.
   End induction.
@@ -3190,7 +3211,6 @@ Section ltype_def.
               ltype_own_core lt_full (Uniq κ γ) π (PlaceIn r') l))
       | Shared κ =>
           False
-        (*ltype_own lt_cur (Shared κ) π r l*)
       end.
 
   Definition coreable_ltype_own (rec : ltype_own_type) (rec_core : ltype_own_type)
@@ -3218,14 +3238,25 @@ Section ltype_def.
 
   Definition magic_ltype_own
       (rec : ltype_own_type) (rec_core : ltype_own_type)
-      {rt_cur rt_full : Type}
-      (lt_cur : ltype rt_cur) (lt_full : ltype rt_full)
-      (Cpre Cpost : rt_cur → iProp Σ)
-      (k : bor_kind) (π : thread_id) (r : place_rfn rt_full) (l : loc) : iProp Σ :=
-    match k with (* TODO: MagicType *)
-    | Owned wl => False
-    | Uniq κ γ => False
-    | Shared κ => False
+      {rt_cur rt_inner rt_full : Type}
+      (lt_cur : ltype rt_cur) (lt_inner : ltype rt_inner) (lt_full : ltype rt_full)
+      (Cpre : rt_inner → rt_full → iProp Σ) (Cpost : rt_inner → rt_full → iProp Σ)
+      (k : bor_kind) (π : thread_id) (r : place_rfn rt_cur) (l : loc) : iProp Σ :=
+    ∃ ly, ⌜use_layout_alg (ltype_st lt_cur) = Some ly⌝ ∗
+      ⌜l `has_layout_loc` ly⌝ ∗
+      loc_in_bounds l 0 (ly_size ly) ∗
+      ⌜ltype_st lt_cur = ltype_st lt_inner⌝ ∗
+      ⌜ltype_st lt_inner = ltype_st lt_full⌝ ∗
+      match k with
+      | Owned wl =>
+            ltype_own lt_cur (Owned false) π r l ∗
+            logical_step lftE
+            (∀ (r : rt_inner) (r' : rt_full),
+              Cpre r r' -∗
+              (ltype_own lt_inner (Owned false) π (PlaceIn r) l ={lftE}=∗
+              ltype_own_core lt_full (Owned wl) π (PlaceIn r') l ∗
+              Cpost r r'))
+      | _ => False
     end.
 
   Lemma ltype_own_pre_ofty_unfold {rt} (ty : type rt) (core : bool) k π r l :
@@ -3756,16 +3787,33 @@ Section ltype_def.
     intros ?. done.
   Qed.
 
-  Lemma ltype_own_magic_unfold {rt_cur rt_full : Type} (lt_cur : ltype rt_cur) (lt_full : ltype rt_full) (Cpre Cpost : rt_cur → iProp Σ) k π r l :
-    ltype_own (MagicLtype lt_cur lt_full Cpre Cpost) k π r l ≡ magic_ltype_own (@ltype_own) (@ltype_own_core) lt_cur lt_full Cpre Cpost k π r l.
+  Lemma ltype_own_magic_unfold {rt_cur rt_inner rt_full : Type} (lt_cur : ltype rt_cur) (lt_inner : ltype rt_inner) (lt_full : ltype rt_full)
+      (Cpre : rt_inner → rt_full → iProp Σ) (Cpost : rt_inner → rt_full → iProp Σ) k π r l :
+    ltype_own (MagicLtype lt_cur lt_inner lt_full Cpre Cpost) k π r l ≡ magic_ltype_own (@ltype_own) (@ltype_own_core) lt_cur lt_inner lt_full Cpre Cpost k π r l.
   Proof.
     rewrite /magic_ltype_own ?ltype_own_core_unseal /ltype_own_core_def ?ltype_own_unseal /ltype_own_def /ltype_own_pre.
     simp lty_own_pre.
-    done.
+    generalize (ltype_rt_agree lt_cur).
+    generalize (ltype_rt_agree lt_full).
+    generalize (ltype_rt_agree lt_inner).
+    generalize (ltype_rt_agree (MagicLtype lt_cur lt_inner lt_full Cpre Cpost)).
+    simpl.
+    intros Heq1 Heq2 Heq3 Heq4. move : Cpre Cpost r.
+    move: Heq1 Heq2 Heq3 Heq4.
+    intros <- <- <-.
+    intros Heq Cpre Cpost r. specialize (UIP_refl _ _ Heq) => ->. clear Heq.
+    repeat f_equiv.
+    - done.
+    - done.
+    - iSplit.
+      + iIntros "(%Heq1 & %Heq2 & Ha)".
+        rewrite (UIP_refl _ _ Heq1) (UIP_refl _ _ Heq2). done.
+      + iIntros "Ha". iExists eq_refl, eq_refl. done.
   Qed.
-  Lemma ltype_own_core_magic_unfold {rt_cur rt_full : Type} (lt_cur : ltype rt_cur) (lt_full : ltype rt_full) (Cpre Cpost : rt_cur → iProp Σ) k π r l :
-    ltype_own_core (MagicLtype lt_cur lt_full Cpre Cpost) k π r l ≡ magic_ltype_own (@ltype_own) (@ltype_own_core) lt_cur lt_full Cpre Cpost k π r l.
-  Proof. (* TODO? MagicType *)
+  Lemma ltype_own_core_magic_unfold {rt_cur rt_inner rt_full : Type} (lt_cur : ltype rt_cur) (lt_inner : ltype rt_inner) (lt_full : ltype rt_full)
+      (Cpre : rt_inner → rt_full → iProp Σ) (Cpost : rt_inner → rt_full → iProp Σ) k π r l :
+    ltype_own_core (MagicLtype lt_cur lt_inner lt_full Cpre Cpost) k π r l ≡ magic_ltype_own (@ltype_own) (@ltype_own_core) lt_cur lt_inner lt_full Cpre Cpost k π r l.
+  Proof.
     rewrite -ltype_own_magic_unfold.
     rewrite ltype_own_core_unseal ltype_own_unseal /ltype_own_core_def /ltype_own_def /ltype_own_pre.
     simp lty_own_pre. done.
@@ -3870,7 +3918,7 @@ Section ltype_def.
 
   Lemma ltype_own_Owned_true_false {rt} (lt : ltype rt) π r l :
     match ltype_lty lt with
-    | OpenedLty _ _ _ _ _ | CoreableLty _ _ | ShadowedLty _ _ _ | MagicLty _ _ _ _ => False
+    | OpenedLty _ _ _ _ _ | CoreableLty _ _ | ShadowedLty _ _ _ | MagicLty _ _ _ _ _ => False
     | _ => True
     end →
     ltype_own lt (Owned true) π r l -∗
@@ -3882,7 +3930,7 @@ Section ltype_def.
   Qed.
   Lemma ltype_own_Owned_false_true {rt} (lt : ltype rt) π r l :
     match ltype_lty lt with
-    | OpenedLty _ _ _ _ _ | CoreableLty _ _ | ShadowedLty _ _ _ | MagicLty _ _ _ _ => False
+    | OpenedLty _ _ _ _ _ | CoreableLty _ _ | ShadowedLty _ _ _ | MagicLty _ _ _ _ _ => False
     | _ => True
     end →
     ltype_own lt (Owned false) π r l -∗
@@ -4034,8 +4082,8 @@ Section ltype_def.
     - apply UIP_t.
     - apply proof_irrelevance.
   Qed.
-  Lemma ltype_core_magic {rt_cur rt_full} (lt_cur : ltype rt_cur) (lt_full : ltype rt_full) Cpre Cpost :
-    ltype_core (MagicLtype lt_cur lt_full Cpre Cpost) = ltype_core lt_full.
+  Lemma ltype_core_magic {rt_cur rt_inner rt_full} (lt_cur : ltype rt_cur) (lt_inner : ltype rt_inner) (lt_full : ltype rt_full) Cpre Cpost :
+    ltype_core (MagicLtype lt_cur lt_inner lt_full Cpre Cpost) = MagicLtype lt_cur lt_inner lt_full Cpre Cpost.
   Proof.
     rewrite /ltype_core /MagicLtype /=.
     f_equiv; simpl.
@@ -4091,8 +4139,8 @@ Section ltype_def.
   Lemma ltype_st_shadowed {rt_cur rt_full} (lt_cur : ltype rt_cur) (r_cur : place_rfn rt_cur) (lt_full : ltype rt_full) :
     ltype_st (ShadowedLtype lt_cur r_cur lt_full) = ltype_st lt_full.
   Proof. done. Qed.
-  Lemma ltype_st_magic {rt_cur rt_full} (lt_cur : ltype rt_cur) (lt_full : ltype rt_full) Cpre Cpost :
-    ltype_st (MagicLtype lt_cur lt_full Cpre Cpost) = ltype_st lt_full.
+  Lemma ltype_st_magic {rt_cur rt_inner rt_full} (lt_cur : ltype rt_cur) (lt_inner : ltype rt_inner) (lt_full : ltype rt_full) Cpre Cpost :
+    ltype_st (MagicLtype lt_cur lt_inner lt_full Cpre Cpost) = ltype_st lt_cur.
   Proof. done. Qed.
 
   (** Lifting the core equations to ltypes *)
@@ -4145,7 +4193,7 @@ Section ltype_def.
     | OpenedLty _ _ _ _ _  => []
     | CoreableLty κs _ => κs
     | ShadowedLty lt_cur r_cur lt_full => lty_blocked_lfts lt_full
-    | MagicLty _ _ _ _ => []
+    | MagicLty _ _ _ _ _ => []
     end.
 
   Definition ltype_blocked_lfts {rt} (lt : ltype rt) : list lft :=
@@ -4174,7 +4222,7 @@ Section ltype_def.
     | CoreableLty _ _ => True
     | ShadowedLty lt _ _ =>
         False
-    | MagicLty _ _ _ _ => False
+    | MagicLty _ _ _ _ _ => False
     end.
   Definition ltype_uniq_deinitializable {rt} (lt : ltype rt) :=
     lty_uniq_deinitializable lt.(ltype_lty).
@@ -4239,7 +4287,7 @@ Section ltype_def.
     | CoreableLty _ _ => Some None
     | ShadowedLty lt _ _ =>
         None
-    | MagicLty _ _ _ _ => None
+    | MagicLty _ _ _ _ _ => None
     end.
   Definition ltype_uniq_extractable {rt} (lt : ltype rt) : option (option lft) :=
     lty_uniq_extractable lt.(ltype_lty).
@@ -4348,7 +4396,7 @@ Ltac simp_ltype_core Heq :=
       rewrite (ltype_core_coreable) in Heq
   | _ = ltype_core (ShadowedLtype _ _ _) =>
       rewrite (ltype_core_shadowed _ _ _) in Heq
-  | _ = ltype_core (MagicLtype _ _ _ _) =>
+  | _ = ltype_core (MagicLtype _ _ _ _ _) =>
       rewrite (ltype_core_magic) in Heq
   end.
 Ltac simp_ltype_st Heq :=
@@ -5506,16 +5554,12 @@ Section blocked.
       rewrite -ltype_own_core_equiv. iApply ("Ha2" with "Hdead Hb").
   Qed.
 
-  Lemma magic_ltype_imp_unblockable {rt_cur rt_full} (lt_cur : ltype rt_cur) (lt_full : ltype rt_full) Cpre Cpost κs :
-    ⊢ imp_unblockable κs (MagicLtype lt_cur lt_full Cpre Cpost).
-  Proof. (* TODO: MagicType *)
+  Lemma magic_ltype_imp_unblockable {rt_cur rt_inner rt_full} (lt_cur : ltype rt_cur) (lt_inner : ltype rt_inner) (lt_full : ltype rt_full) Cpre Cpost κs :
+    ⊢ imp_unblockable κs (MagicLtype lt_cur lt_inner lt_full Cpre Cpost).
+  Proof.
     iModIntro. iSplitL.
-    - iIntros (κ' ????) "#Hdead Hb".
-      rewrite ltype_own_core_magic_unfold ltype_own_magic_unfold /magic_ltype_own.
-      done.
-    - iIntros (????) "#Hdead Ha".
-      rewrite ltype_own_core_magic_unfold ltype_own_magic_unfold /magic_ltype_own.
-      done.
+    - iIntros (κ' ????). rewrite ltype_own_core_equiv ltype_core_magic. eauto.
+    - iIntros (????). rewrite ltype_own_core_equiv ltype_core_magic. eauto.
   Qed.
 
   (** Once all the blocked lifetimes are dead, every ltype is unblockable to its core. *)
@@ -5568,7 +5612,7 @@ Section blocked.
     - iIntros (rt_full κ' lt_full Hdead). iApply coreable_ltype_imp_unblockable.
     - iIntros (rt_cur rt_full lt_cur r_cur lt_full _ Hub).
       iApply shadowed_ltype_imp_unblockable. done.
-    - iIntros (rt_cur rt_full lt_cur lt_full Cpre Cpost IH1 IH2).
+    - iIntros (rt_cur rt_inner rt_full lt_cur lt_inner ty_full Cpre R Cpost IH1 IH2).
       iApply magic_ltype_imp_unblockable.
   Qed.
 
diff --git a/theories/rust_typing/program_rules.v b/theories/rust_typing/program_rules.v
index 73c98c38d75efaf83cfadd21149045811c006361..ed91fb2eb8584dd0d521f28c721206a3cf8a925e 100644
--- a/theories/rust_typing/program_rules.v
+++ b/theories/rust_typing/program_rules.v
@@ -496,7 +496,7 @@ Section typing.
     λ T, i2p (subsume_full_own_loc_owned_false π E L l lt1 lt2 r1 r2 T).
 
   Lemma subsume_full_own_loc_owned_false_true {rt1 rt2} π E L s l (lt1 : ltype rt1) (lt2 : ltype rt2) r1 r2 T
-    `{!TCDone (match ltype_lty _ lt2 with | OpenedLty _ _ _ _ _ | CoreableLty _ _ | ShadowedLty _ _ _ => False | MagicLty _ _ _ _ => False | _ => True end)} :
+    `{!TCDone (match ltype_lty _ lt2 with | OpenedLty _ _ _ _ _ | CoreableLty _ _ | ShadowedLty _ _ _ => False | MagicLty _ _ _ _ _ => False | _ => True end)} :
     prove_with_subtype E L s ProveDirect (have_creds) (λ L2 κs R,
       subsume_full E L2 s (l ◁ₗ[π, Owned false] r1 @ lt1) (l ◁ₗ[π, Owned false] r2 @ lt2) (λ L3 R2, T L3 (R ∗ R2)))
     ⊢ subsume_full E L s (l ◁ₗ[π, Owned false] r1 @ lt1) (l ◁ₗ[π, Owned true] r2 @ lt2) T.
@@ -512,12 +512,12 @@ Section typing.
     iApply (ltype_own_Owned_false_true with "Hl Hcred"); done.
   Qed.
   Global Instance subsume_full_own_loc_owned_false_true_inst {rt1 rt2} π E L s l (lt1 : ltype rt1) (lt2 : ltype rt2) r1 r2
-    `{!TCDone (match ltype_lty _ lt2 with | OpenedLty _ _ _ _ _ | CoreableLty _ _ | ShadowedLty _ _ _ => False | MagicLty _ _ _ _ => False | _ => True end)} :
+    `{!TCDone (match ltype_lty _ lt2 with | OpenedLty _ _ _ _ _ | CoreableLty _ _ | ShadowedLty _ _ _ => False | MagicLty _ _ _ _ _ => False | _ => True end)} :
     SubsumeFull E L s (l ◁ₗ[π, Owned false] r1 @ lt1) (l ◁ₗ[π, Owned true] r2 @ lt2) | 1001 :=
     λ T, i2p (subsume_full_own_loc_owned_false_true π E L s l lt1 lt2 r1 r2 T).
 
   Lemma subsume_full_own_loc_owned_true_false {rt1 rt2} π E L s l (lt1 : ltype rt1) (lt2 : ltype rt2) r1 r2 T
-    `{!TCDone (match ltype_lty _ lt1 with | OpenedLty _ _ _ _ _ | CoreableLty _ _ | ShadowedLty _ _ _ => False | MagicLty _ _ _ _ => False | _ => True end)} :
+    `{!TCDone (match ltype_lty _ lt1 with | OpenedLty _ _ _ _ _ | CoreableLty _ _ | ShadowedLty _ _ _ => False | MagicLty _ _ _ _ _ => False | _ => True end)} :
       introduce_with_hooks E L (£ (num_cred - 1) ∗ atime 1) (λ L2,
       subsume_full E L2 s (l ◁ₗ[π, Owned false] r1 @ lt1) (l ◁ₗ[π, Owned false] r2 @ lt2) T)
     ⊢ subsume_full E L s (l ◁ₗ[π, Owned true] r1 @ lt1) (l ◁ₗ[π, Owned false] r2 @ lt2) T.
@@ -529,7 +529,7 @@ Section typing.
     by iApply ("HT" with "[//] [//] CTX HE HL").
   Qed.
   Global Instance subsume_full_own_loc_owned_true_false_inst {rt1 rt2} π E L s l (lt1 : ltype rt1) (lt2 : ltype rt2) r1 r2
-    `{!TCDone (match ltype_lty _ lt1 with | OpenedLty _ _ _ _ _ | CoreableLty _ _ | ShadowedLty _ _ _ => False | MagicLty _ _ _ _ => False | _ => True end)} :
+    `{!TCDone (match ltype_lty _ lt1 with | OpenedLty _ _ _ _ _ | CoreableLty _ _ | ShadowedLty _ _ _ => False | MagicLty _ _ _ _ _ => False | _ => True end)} :
     SubsumeFull E L s (l ◁ₗ[π, Owned true] r1 @ lt1) (l ◁ₗ[π, Owned false] r2 @ lt2) | 1001 :=
     λ T, i2p (subsume_full_own_loc_owned_true_false π E L s l lt1 lt2 r1 r2 T).
 
diff --git a/theories/rust_typing/programs.v b/theories/rust_typing/programs.v
index 4026cf9d7f0bfc26fc4af03b21188b7e06bb439e..aed3e9af759bbb66a5cb3ec14fbc4d46fa9f7e2a 100644
--- a/theories/rust_typing/programs.v
+++ b/theories/rust_typing/programs.v
@@ -2121,7 +2121,7 @@ Section judgments.
         (*owned_subltype_step E L false (l ◁ₗ[π, bk'] r' @ lt') (l ◁ₗ[π, bk] r @ ◁ ty) T*)
         match bk' with
         | Owned wl =>
-          prove_with_subtype E L2 false ProveDirect (maybe_creds (negb wl) ∗ ⌜if negb wl then match ltype_lty rt2 lt2 with | OpenedLty _ _ _ _ _ | CoreableLty _ _ | ShadowedLty _ _ _ => False | MagicLty _ _ _ _ => False | _ => True end else True⌝) (λ L3 κs2 R3,
+          prove_with_subtype E L2 false ProveDirect (maybe_creds (negb wl) ∗ ⌜if negb wl then match ltype_lty rt2 lt2 with | OpenedLty _ _ _ _ _ | CoreableLty _ _ | ShadowedLty _ _ _ => False | MagicLty _ _ _ _ _ => False | _ => True end else True⌝) (λ L3 κs2 R3,
             match ltype_blocked_lfts lt2 with
             | [] =>
                 (* we could unblock everything, directly subsume *)