diff --git a/_CoqProject b/_CoqProject
index d25c14ab402b17a7bfcc097392e40b753158cdf1..4de595c58b5312cf83897421606bde48ebf14d3b 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -43,6 +43,8 @@ theories/typing/borrow.v
 theories/typing/cont.v
 theories/typing/fixpoint.v
 theories/typing/type_sum.v
+theories/typing/typing.v
+theories/typing/soundness.v
 theories/typing/tests/get_x.v
 theories/typing/tests/rebor.v
 theories/typing/tests/unbox.v
diff --git a/opam.pins b/opam.pins
index cbfb3aa037aaf068ab5c6b5ed9bf78b1af6e11cd..57ff8356b08651946fb3ba8216c4bfb18c6504e8 100644
--- a/opam.pins
+++ b/opam.pins
@@ -1 +1 @@
-coq-iris https://gitlab.mpi-sws.org/FP/iris-coq be81fb92a76f31ca656f8dad37122843f58884cf
+coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 9fa0b57d44cbba40d7bb272b45cc0875bc68940d
diff --git a/theories/lang/tactics.v b/theories/lang/tactics.v
index 5767645f97ef27cebbde9e9758b5cd3f58d2cddf..99dc74648ca31bca924fd04e2d46dfb1beb3bafe 100644
--- a/theories/lang/tactics.v
+++ b/theories/lang/tactics.v
@@ -240,7 +240,7 @@ Ltac reshape_val e tac :=
   | of_val ?v => v
   | Lit ?l => constr:(LitV l)
   | Rec ?f ?xl ?e => constr:(RecV f xl e)
-  end in let v := go e in first [tac v | fail 2].
+  end in let v := go e in tac v.
 
 Ltac reshape_expr e tac :=
   let rec go_fun K f vs es :=
diff --git a/theories/lifetime/lifetime_sig.v b/theories/lifetime/lifetime_sig.v
index 52fdd1f33ec16810db02af1ec5e1be26f2237a5c..d9f55c4d36cadebe124320885299f4880d286df2 100644
--- a/theories/lifetime/lifetime_sig.v
+++ b/theories/lifetime/lifetime_sig.v
@@ -151,7 +151,7 @@ Module Type lifetime_sig.
   End properties.
 
   Parameter lftΣ : gFunctors.
-  Global Declare Instance subG_lftΣ Σ : subG lftΣ Σ → lftPreG Σ.
+  Global Declare Instance subG_lftPreG Σ : subG lftΣ Σ → lftPreG Σ.
 
   Parameter lft_init : ∀ `{invG Σ, !lftPreG Σ} E, ↑lftN ⊆ E →
     True ={E}=∗ ∃ _ : lftG Σ, lft_ctx.
diff --git a/theories/lifetime/model/definitions.v b/theories/lifetime/model/definitions.v
index a84788de8bb7c3fb1653c245f848e51526f2b5d7..d5677a8513b7846150c82bd2473e74c8a42af463 100644
--- a/theories/lifetime/model/definitions.v
+++ b/theories/lifetime/model/definitions.v
@@ -54,7 +54,7 @@ Definition lftPreG' := lftPreG.
 Definition lftΣ : gFunctors :=
   #[ boxΣ; GFunctor (authR alftUR); GFunctor (authR ilftUR);
      GFunctor (authR borUR); GFunctor (authR natUR); GFunctor (authR inhUR) ].
-Instance subG_lftΣ Σ :
+Instance subG_lftPreG Σ :
   subG lftΣ Σ → lftPreG Σ.
 Proof. solve_inG. Qed.
 
diff --git a/theories/typing/borrow.v b/theories/typing/borrow.v
index 76a658d4d8dbbfa047dbf592ab6330f1ad3171c0..3f114dc3c0ea74182751e594192563f3cbea6362 100644
--- a/theories/typing/borrow.v
+++ b/theories/typing/borrow.v
@@ -1,6 +1,6 @@
 From iris.proofmode Require Import tactics.
 From iris.base_logic Require Import big_op.
-From lrust.lang Require Import heap.
+From lrust.lang Require Import proofmode.
 From lrust.typing Require Export uniq_bor shr_bor own.
 From lrust.typing Require Import lft_contexts type_context programs.
 Set Default Proof Using "Type".
@@ -13,7 +13,7 @@ Section borrow.
   Context `{typeG Σ}.
 
   Lemma tctx_borrow E L p n ty κ :
-    tctx_incl E L [p ◁ own n ty] [p ◁ &uniq{κ}ty; p ◁{κ} own n ty].
+    tctx_incl E L [p ◁ own_ptr n ty] [p ◁ &uniq{κ}ty; p ◁{κ} own_ptr n ty].
   Proof.
     iIntros (tid ??) "#LFT $ $ H".
     rewrite /tctx_interp big_sepL_singleton big_sepL_cons big_sepL_singleton.
@@ -27,8 +27,8 @@ Section borrow.
 
   Lemma tctx_extract_hasty_borrow E L p n ty ty' κ T :
     subtype E L ty' ty →
-    tctx_extract_hasty E L p (&uniq{κ}ty) ((p ◁ own n ty')::T)
-                       ((p ◁{κ} own n ty)::T).
+    tctx_extract_hasty E L p (&uniq{κ}ty) ((p ◁ own_ptr n ty')::T)
+                       ((p ◁{κ} own_ptr n ty)::T).
   Proof.
     intros. apply (tctx_incl_frame_r _ [_] [_;_]). rewrite subtype_tctx_incl.
     by apply tctx_borrow. by f_equiv.
@@ -37,8 +37,8 @@ Section borrow.
   (* See the comment above [tctx_extract_hasty_share] in [uniq_bor.v]. *)
   Lemma tctx_extract_hasty_borrow_share E L p ty ty' κ n T :
     lctx_lft_alive E L κ → subtype E L ty' ty →
-    tctx_extract_hasty E L p (&shr{κ}ty) ((p ◁ own n ty')::T)
-                       ((p ◁ &shr{κ}ty')::(p ◁{κ} own n ty')::T).
+    tctx_extract_hasty E L p (&shr{κ}ty) ((p ◁ own_ptr n ty')::T)
+                       ((p ◁ &shr{κ}ty')::(p ◁{κ} own_ptr n ty')::T).
   Proof.
     intros. apply (tctx_incl_frame_r _ [_] [_;_;_]). rewrite ->tctx_borrow.
     apply (tctx_incl_frame_r _ [_] [_;_]). rewrite ->tctx_share; solve_typing.
@@ -46,7 +46,7 @@ Section borrow.
 
   Lemma type_deref_uniq_own_instr {E L} κ p n ty :
     lctx_lft_alive E L κ →
-    typed_instruction_ty E L [p ◁ &uniq{κ} own n ty] (!p) (&uniq{κ} ty).
+    typed_instruction_ty E L [p ◁ &uniq{κ} own_ptr n ty] (!p) (&uniq{κ} ty).
   Proof.
     iIntros (Hκ) "!#". iIntros (tid qE) "#HEAP #LFT $ HE HL Hp".
     rewrite tctx_interp_singleton.
@@ -70,7 +70,7 @@ Section borrow.
 
   Lemma type_deref_uniq_own {E L} κ x p e n ty C T T' :
     Closed (x :b: []) e →
-    tctx_extract_hasty E L p (&uniq{κ} own n ty) T T' →
+    tctx_extract_hasty E L p (&uniq{κ} own_ptr n ty) T T' →
     lctx_lft_alive E L κ →
     (∀ (v:val), typed_body E L C ((v ◁ &uniq{κ} ty) :: T') (subst' x v e)) →
     typed_body E L C T (let: x := !p in e).
@@ -80,7 +80,7 @@ Section borrow.
 
   Lemma type_deref_shr_own_instr {E L} κ p n ty :
     lctx_lft_alive E L κ →
-    typed_instruction_ty E L [p ◁ &shr{κ} own n ty] (!p) (&shr{κ} ty).
+    typed_instruction_ty E L [p ◁ &shr{κ} own_ptr n ty] (!p) (&shr{κ} ty).
   Proof.
     iIntros (Hκ) "!#". iIntros (tid qE) "#HEAP #LFT $ HE HL Hp".
     rewrite tctx_interp_singleton.
@@ -99,7 +99,7 @@ Section borrow.
 
   Lemma type_deref_shr_own {E L} κ x p e n ty C T T' :
     Closed (x :b: []) e →
-    tctx_extract_hasty E L p (&shr{κ} own n ty) T T' →
+    tctx_extract_hasty E L p (&shr{κ} own_ptr n ty) T T' →
     lctx_lft_alive E L κ →
     (∀ (v:val), typed_body E L C ((v ◁ &shr{κ} ty) :: T') (subst' x v e)) →
     typed_body E L C T (let: x := !p in e).
diff --git a/theories/typing/fixpoint.v b/theories/typing/fixpoint.v
index 140ad5f141f7d1ce5f20a1c09e2efa315fbf949d..c13c52b5d8b17af1744e7e493ea5b9e8ce34ad25 100644
--- a/theories/typing/fixpoint.v
+++ b/theories/typing/fixpoint.v
@@ -1,3 +1,4 @@
+From lrust.lang Require Import proofmode.
 From lrust.typing Require Export lft_contexts type bool.
 Set Default Proof Using "Type".
 
diff --git a/theories/typing/own.v b/theories/typing/own.v
index 8f64431d7bf85df7b05fb90c931807ed27630a42..7bb2b40cf8c8c379bad582a36834437b4dc05f8e 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -41,7 +41,7 @@ Section own.
       rewrite /= -Qcmult_plus_distr_l -Z2Qc_inj_add /Z.add. do 3 f_equal. lia.
   Qed.
 
-  Program Definition own (n : nat) (ty : type) :=
+  Program Definition own_ptr (n : nat) (ty : type) :=
     {| ty_size := 1;
        ty_own tid vl :=
          (* We put a later in front of the †{q}, because we cannot use
@@ -96,7 +96,7 @@ Section own.
   Qed.
 
   Global Instance own_mono E L n :
-    Proper (subtype E L ==> subtype E L) (own n).
+    Proper (subtype E L ==> subtype E L) (own_ptr n).
   Proof.
     intros ty1 ty2 Hincl. iIntros. iSplit; first done.
     iDestruct (Hincl with "* [] [] []") as "(_ & #Ho & #Hs)"; [done..|clear Hincl].
@@ -113,27 +113,27 @@ Section own.
       iMod "Hvs'" as "[Hshr $]". iApply ("Hs" with "Hshr").
   Qed.
   Lemma own_mono' E L n ty1 ty2 :
-    subtype E L ty1 ty2 → subtype E L (own n ty1) (own n ty2).
+    subtype E L ty1 ty2 → subtype E L (own_ptr n ty1) (own_ptr n ty2).
   Proof. apply own_mono. Qed.
   Global Instance own_proper E L n :
-    Proper (eqtype E L ==> eqtype E L) (own n).
+    Proper (eqtype E L ==> eqtype E L) (own_ptr n).
   Proof. intros ?? Heq. split; f_equiv; apply Heq. Qed.
   Lemma own_proper' E L n ty1 ty2 :
-    eqtype E L ty1 ty2 → eqtype E L (own n ty1) (own n ty2).
+    eqtype E L ty1 ty2 → eqtype E L (own_ptr n ty1) (own_ptr n ty2).
   Proof. apply own_proper. Qed.
 
-  Global Instance own_contractive n : Contractive (own n).
+  Global Instance own_contractive n : Contractive (own_ptr n).
   Proof.
     intros m ?? EQ. split; [split|]; simpl.
     - done.
     - destruct m=>// tid vl /=. repeat (apply EQ || f_contractive || f_equiv).
     - intros κ tid l. repeat (apply EQ || f_contractive || f_equiv).
   Qed.
-  Global Instance own_ne n m : Proper (dist m ==> dist m) (own n).
+  Global Instance own_ne n m : Proper (dist m ==> dist m) (own_ptr n).
   Proof. apply contractive_ne, _. Qed.
 
   Global Instance own_send n ty :
-    Send ty → Send (own n ty).
+    Send ty → Send (own_ptr n ty).
   Proof.
     iIntros (Hsend tid1 tid2 vl) "H". iDestruct "H" as (l) "[% [Hm H†]]". subst vl.
     iExists _. iSplit; first done. iFrame "H†". iNext.
@@ -141,7 +141,7 @@ Section own.
   Qed.
 
   Global Instance own_sync n ty :
-    Sync ty → Sync (own n ty).
+    Sync ty → Sync (own_ptr n ty).
   Proof.
     iIntros (Hsync κ tid1 tid2 l) "H". iDestruct "H" as (l') "[Hm #Hshr]".
     iExists _. iFrame "Hm". iAlways. iIntros (F q) "% Htok".
@@ -151,14 +151,14 @@ Section own.
   Qed.
 End own.
 
-Notation box ty := (own ty.(ty_size) ty).
+Notation box ty := (own_ptr ty.(ty_size) ty).
 
 Section typing.
   Context `{typeG Σ}.
 
   (** Typing *)
   Lemma write_own {E L} ty ty' n :
-    ty.(ty_size) = ty'.(ty_size) → typed_write E L (own n ty') ty (own n ty).
+    ty.(ty_size) = ty'.(ty_size) → typed_write E L (own_ptr n ty') ty (own_ptr n ty).
   Proof.
     iIntros (Hsz) "!#". iIntros (p tid F qE qL ?) "_ $ $ Hown". iDestruct "Hown" as (l) "(Heq & H↦ & H†)".
     iDestruct "Heq" as %[= ->]. iDestruct "H↦" as (vl) "[>H↦ Hown]".
@@ -169,7 +169,7 @@ Section typing.
   Qed.
 
   Lemma read_own_copy E L ty n :
-    Copy ty → typed_read E L (own n ty) ty (own n ty).
+    Copy ty → typed_read E L (own_ptr n ty) ty (own_ptr n ty).
   Proof.
     iIntros (Hsz) "!#". iIntros (p tid F qE qL ?) "_ $ $ $ Hown". iDestruct "Hown" as (l) "(Heq & H↦ & H†)".
     iDestruct "Heq" as %[= ->]. iDestruct "H↦" as (vl) "[>H↦ #Hown]". iModIntro.
@@ -178,7 +178,7 @@ Section typing.
   Qed.
 
   Lemma read_own_move E L ty n :
-    typed_read E L (own n ty) ty (own n $ uninit ty.(ty_size)).
+    typed_read E L (own_ptr n ty) ty (own_ptr n $ uninit ty.(ty_size)).
   Proof.
     iAlways. iIntros (p tid F qE qL ?) "_ $ $ $ Hown". iDestruct "Hown" as (l) "(Heq & H↦ & H†)".
     iDestruct "Heq" as %[= ->]. iDestruct "H↦" as (vl) "[>H↦ Hown]".
@@ -191,7 +191,7 @@ Section typing.
   Lemma type_new_instr {E L} (n : Z) :
     0 ≤ n →
     let n' := Z.to_nat n in
-    typed_instruction_ty E L [] (new [ #n ]%E) (own n' (uninit n')).
+    typed_instruction_ty E L [] (new [ #n ]%E) (own_ptr n' (uninit n')).
   Proof.
     intros. iAlways. iIntros (tid q) "#HEAP #LFT $ $ $ _".
     iApply (wp_new with "HEAP"); try done. iModIntro.
@@ -213,7 +213,7 @@ Section typing.
     0 ≤ n →
     let n' := Z.to_nat n in
     subtype E L (uninit n') ty →
-    (∀ (v : val), typed_body E L C ((v ◁ own n' ty) :: T) (subst' x v e)) →
+    (∀ (v : val), typed_body E L C ((v ◁ own_ptr n' ty) :: T) (subst' x v e)) →
     typed_body E L C T (let: x := new [ #n ] in e).
   Proof.
     intros ???? Htyp. eapply type_let. done. by apply type_new_instr. solve_typing.
@@ -238,7 +238,7 @@ Section typing.
 
   Lemma type_delete {E L} ty C T T' (n' : nat) (n : Z)  p e :
     Closed [] e →
-    tctx_extract_hasty E L p (own n' ty) T T' →
+    tctx_extract_hasty E L p (own_ptr n' ty) T T' →
     n = n' → Z.of_nat (ty.(ty_size)) = n →
     typed_body E L C T' e →
     typed_body E L C T (delete [ #n; p ] ;; e).
@@ -251,7 +251,7 @@ Section typing.
     Closed [] p → Closed (x :b: []) e →
     tctx_extract_hasty E L p ty T T' →
     ty.(ty_size) = 1%nat →
-    (∀ (v : val), typed_body E L C ((v ◁ own 1 ty)::T') (subst x v e)) →
+    (∀ (v : val), typed_body E L C ((v ◁ own_ptr 1 ty)::T') (subst x v e)) →
     typed_body E L C T (letalloc: x <- p in e).
   Proof.
     intros. eapply type_new.
@@ -273,7 +273,7 @@ Section typing.
     typed_read E L ty1 ty ty2 →
     tctx_extract_hasty E L p ty1 T T' →
     (∀ (v : val),
-        typed_body E L C ((v ◁ own (ty.(ty_size)) ty)::(p ◁ ty2)::T') (subst x v e)) →
+        typed_body E L C ((v ◁ own_ptr (ty.(ty_size)) ty)::(p ◁ ty2)::T') (subst x v e)) →
     typed_body E L C T (letalloc: x <⋯ !{ty.(ty_size)}p in e).
   Proof.
     intros. eapply type_new.
diff --git a/theories/typing/product_split.v b/theories/typing/product_split.v
index e06f82a5524b72bcc23326b09f224752957e2404..80b4f8656c3321852900fbca7625718e08a27992 100644
--- a/theories/typing/product_split.v
+++ b/theories/typing/product_split.v
@@ -85,8 +85,8 @@ Section product_split.
 
   (** Owned pointers *)
   Lemma tctx_split_own_prod2 E L p n ty1 ty2 :
-    tctx_incl E L [p ◁ own n $ product2 ty1 ty2]
-                  [p ◁ own n ty1; p +ₗ #ty1.(ty_size) ◁ own n ty2].
+    tctx_incl E L [p ◁ own_ptr n $ product2 ty1 ty2]
+                  [p ◁ own_ptr n ty1; p +ₗ #ty1.(ty_size) ◁ own_ptr n ty2].
   Proof.
     iIntros (tid q1 q2) "#LFT $ $ H".
     rewrite tctx_interp_singleton tctx_interp_cons tctx_interp_singleton.
@@ -104,8 +104,8 @@ Section product_split.
   Qed.
 
   Lemma tctx_merge_own_prod2 E L p n ty1 ty2 :
-    tctx_incl E L [p ◁ own n ty1; p +ₗ #ty1.(ty_size) ◁ own n ty2]
-                  [p ◁ own n $ product2 ty1 ty2].
+    tctx_incl E L [p ◁ own_ptr n ty1; p +ₗ #ty1.(ty_size) ◁ own_ptr n ty2]
+                  [p ◁ own_ptr n $ product2 ty1 ty2].
   Proof.
     iIntros (tid q1 q2) "#LFT $ $ H".
     rewrite tctx_interp_singleton tctx_interp_cons tctx_interp_singleton.
@@ -122,13 +122,13 @@ Section product_split.
   Qed.
 
   Lemma own_is_ptr n ty tid (vl : list val) :
-    ty_own (own n ty) tid vl -∗ ⌜∃ l : loc, vl = [(#l) : val]⌝.
+    ty_own (own_ptr n ty) tid vl -∗ ⌜∃ l : loc, vl = [(#l) : val]⌝.
   Proof.
     iIntros "H". iDestruct "H" as (l) "[% _]". iExists l. done.
   Qed.
 
   Lemma tctx_split_own_prod E L n tyl p :
-    tctx_incl E L [p ◁ own n $ product tyl] (hasty_ptr_offsets p (own n) tyl 0).
+    tctx_incl E L [p ◁ own_ptr n $ product tyl] (hasty_ptr_offsets p (own_ptr n) tyl 0).
   Proof.
     apply tctx_split_ptr_prod.
     - intros. apply tctx_split_own_prod2.
@@ -137,8 +137,8 @@ Section product_split.
 
   Lemma tctx_merge_own_prod E L n tyl :
     tyl ≠ [] →
-    ∀ p, tctx_incl E L (hasty_ptr_offsets p (own n) tyl 0)
-                   [p ◁ own n $ product tyl].
+    ∀ p, tctx_incl E L (hasty_ptr_offsets p (own_ptr n) tyl 0)
+                   [p ◁ own_ptr n $ product tyl].
   Proof.
     intros. apply tctx_merge_ptr_prod; try done.
     - apply _.
@@ -266,8 +266,8 @@ Section product_split.
      automation system to be able to perform e.g., borrowing or splitting after
      splitting. *)
   Lemma tctx_extract_split_own_prod E L p p' n ty tyl T T' :
-    tctx_extract_hasty E L p' ty (hasty_ptr_offsets p (own n) tyl 0) T' →
-    tctx_extract_hasty E L p' ty ((p ◁ own n $ Π tyl) :: T) (T' ++ T).
+    tctx_extract_hasty E L p' ty (hasty_ptr_offsets p (own_ptr n) tyl 0) T' →
+    tctx_extract_hasty E L p' ty ((p ◁ own_ptr n $ Π tyl) :: T) (T' ++ T).
   Proof.
     intros. apply (tctx_incl_frame_r T [_] (_::_)). by rewrite tctx_split_own_prod.
   Qed.
@@ -311,8 +311,8 @@ Section product_split.
 
   Lemma tctx_extract_merge_own_prod E L p n tyl T T' :
     tyl ≠ [] →
-    extract_tyl E L p (own n) tyl 0 T T' →
-    tctx_extract_hasty E L p (own n (Π tyl)) T T'.
+    extract_tyl E L p (own_ptr n) tyl 0 T T' →
+    tctx_extract_hasty E L p (own_ptr n (Π tyl)) T T'.
   Proof. auto using tctx_extract_merge_ptr_prod, tctx_merge_own_prod. Qed.
 
   Lemma tctx_extract_merge_uniq_prod E L p κ tyl T T' :
@@ -330,7 +330,7 @@ End product_split.
 
 (* We do not want unification to try to unify the definition of these
    types with anything in order to try splitting or merging. *)
-Hint Opaque own uniq_bor shr_bor tctx_extract_hasty : lrust_typing lrust_typing_merge.
+Hint Opaque own_ptr uniq_bor shr_bor tctx_extract_hasty : lrust_typing lrust_typing_merge.
 
 (* We make sure that splitting is tried before borrowing, so that not
    the entire product is borrowed when only a part is needed. *)
diff --git a/theories/typing/programs.v b/theories/typing/programs.v
index 05fff696f58cd993e675974bb44bee24ef5a6a0e..ebff0b3ded888e456937f63d224cc40d724cdb9f 100644
--- a/theories/typing/programs.v
+++ b/theories/typing/programs.v
@@ -1,5 +1,4 @@
 From iris.base_logic Require Import big_op.
-From lrust.lang Require Export notation.
 From lrust.lang Require Import proofmode memcpy.
 From lrust.typing Require Export type lft_contexts type_context cont_context.
 Set Default Proof Using "Type".
diff --git a/theories/typing/soundness.v b/theories/typing/soundness.v
new file mode 100644
index 0000000000000000000000000000000000000000..6f2f7f0494c2ae0b5ebff45678213f8cb1dda609
--- /dev/null
+++ b/theories/typing/soundness.v
@@ -0,0 +1,78 @@
+From iris.algebra Require Import frac.
+From iris.base_logic Require Import big_op.
+From iris.base_logic.lib Require Import na_invariants.
+From iris.proofmode Require Import tactics.
+From lrust.lang Require Import races adequacy proofmode notation.
+From lrust.lifetime Require Import lifetime frac_borrow.
+From lrust.typing Require Import typing.
+
+Set Default Proof Using "Type".
+
+Class typePreG Σ := PreTypeG {
+  type_heapG :> heapPreG Σ;
+  type_lftG :> lftPreG Σ;
+  type_preG_na_invG :> na_invG Σ;
+  type_frac_borrowG :> frac_borG Σ
+}.
+
+Definition typeΣ : gFunctors :=
+  #[heapΣ; lftΣ; na_invΣ; GFunctor (constRF fracR)].
+Instance subG_typePreG {Σ} : subG typeΣ Σ → typePreG Σ.
+Proof.
+  split.
+  - apply subG_heapPreG. solve_inG.
+  - apply subG_lftPreG. solve_inG.
+  - solve_inG.
+  - solve_inG.
+Qed.
+
+Section type_soundness.
+  Definition exit_cont : val := λ: [<>], #().
+
+  Definition main_type `{typeG Σ} :=
+    fn (λ _, []) (λ _, [# ]) (λ _:(), box unit).
+
+  Theorem type_soundness `{typePreG Σ} (main : val) σ t :
+    (∀ `{typeG Σ}, typed_instruction_ty [] [] [] main main_type) →
+    rtc step ([main [exit_cont]%E], ∅) (t, σ) →
+    nonracing_threadpool t σ ∧
+    (∀ e, e ∈ t → is_Some (to_val e) ∨ reducible e σ).
+  Proof.
+    intros Hmain Hrtc.
+    cut (adequate (main [exit_cont]%E) ∅ (λ _, True)).
+    { split. by eapply adequate_nonracing.
+      intros. by eapply (adequate_safe (main [exit_cont]%E)). }
+    apply: heap_adequacy=>?.
+    iIntros "!# #HEAP". iMod lft_init as (?) "#LFT". done.
+    iMod na_alloc as (tid) "Htl". set (Htype := TypeG _ _ _ _ _).
+    wp_bind (of_val main). iApply (wp_wand with "[Htl]").
+    iApply (Hmain _ $! tid 1%Qp with "* HEAP LFT Htl [] [] []").
+    { by rewrite /elctx_interp big_sepL_nil. }
+    { by rewrite /llctx_interp big_sepL_nil. }
+    { by rewrite tctx_interp_nil. }
+    clear Hrtc Hmain main. iIntros (main) "(Htl & _ & _ & Hmain)".
+    rewrite tctx_interp_singleton. iDestruct "Hmain" as (?) "[EQ Hmain]".
+    rewrite eval_path_of_val. iDestruct "EQ" as %[= <-].
+    iDestruct "Hmain" as (f k x e ?) "(EQ & % & Hmain)". iDestruct "EQ" as %[= ->].
+    destruct x; try done.
+    iApply (wp_rec _ _ _ _ _ _ [exit_cont]%E); [done| |by simpl_subst|iNext].
+    { repeat econstructor. apply to_of_val. }
+    iApply ("Hmain" $! () exit_cont [#] tid 1%Qp with "HEAP LFT Htl [] [] []");
+      last by rewrite tctx_interp_nil.
+    { by rewrite /elctx_interp big_sepL_nil. }
+    { by rewrite /llctx_interp big_sepL_nil. }
+    iIntros "_". rewrite cctx_interp_singleton. simpl. iIntros (args) "_ _".
+    inv_vec args. iIntros (x) "_". by wp_seq.
+  Qed.
+End type_soundness.
+
+(* Soundness theorem when no other CMRA is needed. *)
+
+Theorem type_soundness_closed (main : val) σ t :
+  (∀ `{typeG typeΣ}, typed_instruction_ty [] [] [] main main_type) →
+  rtc step ([main [exit_cont]%E], ∅) (t, σ) →
+  nonracing_threadpool t σ ∧
+  (∀ e, e ∈ t → is_Some (to_val e) ∨ reducible e σ).
+Proof.
+  intros. eapply @type_soundness; try done. apply _.
+Qed.
diff --git a/theories/typing/tests/get_x.v b/theories/typing/tests/get_x.v
index c75329e416a53c1d96c6e25a4eef7b9dfa7d56cf..54577cbf719a740aa5a5ae9010336ac219575041 100644
--- a/theories/typing/tests/get_x.v
+++ b/theories/typing/tests/get_x.v
@@ -1,7 +1,4 @@
-From lrust.lifetime Require Import definitions.
-From lrust.lang Require Import new_delete.
-From lrust.typing Require Import programs product product_split own uniq_bor
-                    shr_bor int function lft_contexts uninit cont.
+From lrust.typing Require Import typing.
 Set Default Proof Using "Type".
 
 Section get_x.
diff --git a/theories/typing/tests/init_prod.v b/theories/typing/tests/init_prod.v
index 145c9471ff250ea5bb961dc104d05d4486b0b340..8893096ace2ede3ecf2789f100cf01ece7eab906 100644
--- a/theories/typing/tests/init_prod.v
+++ b/theories/typing/tests/init_prod.v
@@ -1,7 +1,4 @@
-From lrust.lifetime Require Import definitions.
-From lrust.lang Require Import new_delete.
-From lrust.typing Require Import programs product product_split own uniq_bor
-                    shr_bor int function lft_contexts uninit cont borrow.
+From lrust.typing Require Import typing.
 Set Default Proof Using "Type".
 
 Section init_prod.
@@ -23,7 +20,7 @@ Section init_prod.
     eapply type_deref; [solve_typing..|apply read_own_move|done|]=>y'. simpl_subst.
     eapply (type_new_subtype (Π[uninit 1; uninit 1])); [solve_typing..|].
       intros r. simpl_subst. unfold Z.to_nat, Pos.to_nat; simpl.
-    eapply (type_assign (own 2 (uninit 1))); [solve_typing..|by apply write_own|].
+    eapply (type_assign (own_ptr 2 (uninit 1))); [solve_typing..|by apply write_own|].
     eapply type_assign; [solve_typing..|by apply write_own|].
     eapply type_delete; [solve_typing..|].
     eapply type_delete; [solve_typing..|].
diff --git a/theories/typing/tests/lazy_lft.v b/theories/typing/tests/lazy_lft.v
index 4e5da308eeb959b98d644e498d80aa05577ce01b..aa147026c2c51b4ab7cf84e5213ca659a20c68df 100644
--- a/theories/typing/tests/lazy_lft.v
+++ b/theories/typing/tests/lazy_lft.v
@@ -1,7 +1,4 @@
-From lrust.lifetime Require Import definitions.
-From lrust.lang Require Import new_delete.
-From lrust.typing Require Import programs product product_split own uniq_bor
-                    shr_bor int function lft_contexts uninit cont borrow type_sum.
+From lrust.typing Require Import typing.
 Set Default Proof Using "Type".
 
 Section lazy_lft.
diff --git a/theories/typing/tests/option_as_mut.v b/theories/typing/tests/option_as_mut.v
index 1c57578df2531c8f113f10e26ab3b1975a02a25c..114f89f1663a4adb37d55b07dde8b438a74f42c6 100644
--- a/theories/typing/tests/option_as_mut.v
+++ b/theories/typing/tests/option_as_mut.v
@@ -1,7 +1,4 @@
-From lrust.lifetime Require Import definitions.
-From lrust.lang Require Import new_delete.
-From lrust.typing Require Import programs product product_split own uniq_bor
-                    shr_bor int function lft_contexts uninit cont borrow type_sum.
+From lrust.typing Require Import typing.
 Set Default Proof Using "Type".
 
 Section option_as_mut.
diff --git a/theories/typing/tests/rebor.v b/theories/typing/tests/rebor.v
index 67cd5cde4dbc5bc37a3f3bab1e15d4f647eee836..a30f43cb7dff0e744797804ba8e3c5a53f72a9ed 100644
--- a/theories/typing/tests/rebor.v
+++ b/theories/typing/tests/rebor.v
@@ -1,7 +1,4 @@
-From lrust.lifetime Require Import definitions.
-From lrust.lang Require Import new_delete.
-From lrust.typing Require Import programs product product_split own uniq_bor
-                    shr_bor int function lft_contexts uninit cont borrow.
+From lrust.typing Require Import typing.
 Set Default Proof Using "Type".
 
 Section rebor.
diff --git a/theories/typing/tests/unbox.v b/theories/typing/tests/unbox.v
index 77f66614dc7123f91a3ad3f316aebe348cc946fe..3f9b02b4cd7866ba6e1175c545ac8378910a690e 100644
--- a/theories/typing/tests/unbox.v
+++ b/theories/typing/tests/unbox.v
@@ -1,7 +1,4 @@
-From lrust.lifetime Require Import definitions.
-From lrust.lang Require Import new_delete.
-From lrust.typing Require Import programs product product_split own uniq_bor
-                    shr_bor int function lft_contexts uninit cont borrow.
+From lrust.typing Require Import typing.
 Set Default Proof Using "Type".
 
 Section unbox.
diff --git a/theories/typing/tests/unwrap_or.v b/theories/typing/tests/unwrap_or.v
index b1c2724c6587c7285cb0fefd7ece87454c9eb209..72a297853b8344d0bb978607d1926a12b471d3f9 100644
--- a/theories/typing/tests/unwrap_or.v
+++ b/theories/typing/tests/unwrap_or.v
@@ -1,7 +1,4 @@
-From lrust.lifetime Require Import definitions.
-From lrust.lang Require Import new_delete.
-From lrust.typing Require Import programs product product_split own uniq_bor
-                    shr_bor int function lft_contexts uninit cont borrow type_sum.
+From lrust.typing Require Import typing.
 Set Default Proof Using "Type".
 
 Section unwrap_or.
diff --git a/theories/typing/type.v b/theories/typing/type.v
index bf270f5b7387dd58285e99e8a567c1c142cc1f6b..979af897b555b8e431be990bae3bf814fd375e9e 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -9,7 +9,7 @@ Class typeG Σ := TypeG {
   type_heapG :> heapG Σ;
   type_lftG :> lftG Σ;
   type_na_invG :> na_invG Σ;
-  type_frac_borrowG Σ :> frac_borG Σ
+  type_frac_borrowG :> frac_borG Σ
 }.
 
 Definition lftE := ↑lftN.
diff --git a/theories/typing/type_context.v b/theories/typing/type_context.v
index 1d1535f1973b77f0affb09743fa6c68be0d91a29..824d0bdee0fefc09cabc224e3e35da820e4d4f58 100644
--- a/theories/typing/type_context.v
+++ b/theories/typing/type_context.v
@@ -1,6 +1,5 @@
 From iris.proofmode Require Import tactics.
 From iris.base_logic Require Import big_op.
-From lrust.lang Require Import notation.
 From lrust.typing Require Import type lft_contexts.
 Set Default Proof Using "Type".
 
diff --git a/theories/typing/type_sum.v b/theories/typing/type_sum.v
index 037176e2d36a03c3e99fa27fdef7aa448002f833..e1017869dc366250590c852f0c97512e9ab8ee13 100644
--- a/theories/typing/type_sum.v
+++ b/theories/typing/type_sum.v
@@ -1,6 +1,6 @@
 From iris.proofmode Require Import tactics.
-From lrust.lang Require Import heap memcpy.
-From lrust.typing Require Export uninit uniq_bor shr_bor own sum.
+From lrust.lang Require Import memcpy.
+From lrust.typing Require Import uninit uniq_bor shr_bor own sum.
 From lrust.typing Require Import lft_contexts type_context programs product.
 Set Default Proof Using "Type".
 
@@ -9,11 +9,11 @@ Section case.
 
   Lemma type_case_own' E L C T p n tyl el :
     Forall2 (λ ty e,
-      typed_body E L C ((p +ₗ #0 ◁ own n (uninit 1)) :: (p +ₗ #1 ◁ own n ty) ::
+      typed_body E L C ((p +ₗ #0 ◁ own_ptr n (uninit 1)) :: (p +ₗ #1 ◁ own_ptr n ty) ::
          (p +ₗ #(S (ty.(ty_size))) ◁
-            own n (uninit (list_max (map ty_size tyl) - ty_size ty))) :: T) e ∨
-      typed_body E L C ((p ◁ own n (sum tyl)) :: T) e) tyl el →
-    typed_body E L C ((p ◁ own n (sum tyl)) :: T) (case: !p of el).
+            own_ptr n (uninit (list_max (map ty_size tyl) - ty_size ty))) :: T) e ∨
+      typed_body E L C ((p ◁ own_ptr n (sum tyl)) :: T) e) tyl el →
+    typed_body E L C ((p ◁ own_ptr n (sum tyl)) :: T) (case: !p of el).
   Proof.
     iIntros (Hel) "!#". iIntros (tid qE) "#HEAP #LFT Hna HE HL HC HT". wp_bind p.
     rewrite tctx_interp_cons. iDestruct "HT" as "[Hp HT]".
@@ -49,12 +49,12 @@ Section case.
   Qed.
 
   Lemma type_case_own E L C T T' p n tyl el :
-    tctx_extract_hasty E L p (own n (sum tyl)) T T' →
+    tctx_extract_hasty E L p (own_ptr n (sum tyl)) T T' →
     Forall2 (λ ty e,
-      typed_body E L C ((p +ₗ #0 ◁ own n (uninit 1)) :: (p +ₗ #1 ◁ own n ty) ::
+      typed_body E L C ((p +ₗ #0 ◁ own_ptr n (uninit 1)) :: (p +ₗ #1 ◁ own_ptr n ty) ::
          (p +ₗ #(S (ty.(ty_size))) ◁
-            own n (uninit (list_max (map ty_size tyl) - ty_size ty))) :: T') e ∨
-      typed_body E L C ((p ◁ own n (sum tyl)) :: T') e) tyl el →
+            own_ptr n (uninit (list_max (map ty_size tyl) - ty_size ty))) :: T') e ∨
+      typed_body E L C ((p ◁ own_ptr n (sum tyl)) :: T') e) tyl el →
     typed_body E L C T (case: !p of el).
   Proof. unfold tctx_extract_hasty=>->. apply type_case_own'. Qed.
 
diff --git a/theories/typing/unsafe/cell.v b/theories/typing/unsafe/cell.v
index 6219552696c6bf97c12d06656efe87386eb394b9..1c7c8c5cdb5ac4d2d97b2d20fa8d0ad4465e4a78 100644
--- a/theories/typing/unsafe/cell.v
+++ b/theories/typing/unsafe/cell.v
@@ -3,7 +3,7 @@ From iris.base_logic Require Import big_op.
 From lrust.lang Require Import memcpy.
 From lrust.lifetime Require Import na_borrow.
 From lrust.typing Require Export type.
-From lrust.typing Require Import type_context programs shr_bor own function product uninit cont.
+From lrust.typing Require Import typing.
 Set Default Proof Using "Type".
 
 Section cell.