diff --git a/case_studies/minicell/RefinedRust.toml b/case_studies/minicell/RefinedRust.toml
new file mode 100644
index 0000000000000000000000000000000000000000..fec885e2583be49e45ff35588c6a05c8478d5e0a
--- /dev/null
+++ b/case_studies/minicell/RefinedRust.toml
@@ -0,0 +1,2 @@
+output_dir = "./output"
+lib_load_paths = ["../../stdlib"]
diff --git a/case_studies/minicell/dune-project b/case_studies/minicell/dune-project
new file mode 100644
index 0000000000000000000000000000000000000000..8cf77f06f47ac4228dc62aa390a3a79704680baa
--- /dev/null
+++ b/case_studies/minicell/dune-project
@@ -0,0 +1,3 @@
+(lang dune 3.8)
+(using coq 0.8)
+(name minicell)
diff --git a/case_studies/minicell/output/minicell/proofs/proof_example_test1.v b/case_studies/minicell/output/minicell/proofs/proof_example_test1.v
new file mode 100644
index 0000000000000000000000000000000000000000..e1f17f04853fb788320ca2379b20ade654289f22
--- /dev/null
+++ b/case_studies/minicell/output/minicell/proofs/proof_example_test1.v
@@ -0,0 +1,24 @@
+From caesium Require Import lang notation.
+From refinedrust Require Import typing shims.
+From refinedrust.examples.minicell.generated Require Import generated_code_minicell generated_specs_minicell generated_template_example_test1.
+
+Set Default Proof Using "Type".
+
+Section proof.
+Context `{RRGS : !refinedrustGS Σ}.
+
+Lemma example_test1_proof (Ï€ : thread_id) :
+  example_test1_lemma π.
+Proof.
+  example_test1_prelude.
+
+  repeat liRStep; liShow.
+  liInst Hevar Zeven.
+  repeat liRStep; liShow.
+
+  all: print_remaining_goal.
+  Unshelve. all: sidecond_solver.
+  Unshelve. all: sidecond_hammer.
+  Unshelve. all: print_remaining_sidecond.
+Qed.
+End proof.
diff --git a/case_studies/minicell/output/minicell/proofs/proof_example_test2.v b/case_studies/minicell/output/minicell/proofs/proof_example_test2.v
new file mode 100644
index 0000000000000000000000000000000000000000..1c4fa71ee32d640d13b23d6e3b89a7ef2517c287
--- /dev/null
+++ b/case_studies/minicell/output/minicell/proofs/proof_example_test2.v
@@ -0,0 +1,26 @@
+From caesium Require Import lang notation.
+From refinedrust Require Import typing shims.
+From refinedrust.examples.minicell.generated Require Import generated_code_minicell generated_specs_minicell generated_template_example_test2.
+
+Set Default Proof Using "Type".
+
+Section proof.
+Context `{RRGS : !refinedrustGS Σ}.
+
+Lemma example_test2_proof (Ï€ : thread_id) :
+  example_test2_lemma π.
+Proof.
+  example_test2_prelude.
+
+  repeat liRStep; liShow.
+
+  all: print_remaining_goal.
+  Unshelve. all: sidecond_solver.
+  Unshelve. all: sidecond_hammer.
+  { unsafe_unfold_common_caesium_defs; simpl. lia. }
+  { revert select (Zeven _). revert select (_ `rem` 2 ≠ 0%Z).
+    rewrite Zeven_ex_iff Z.rem_divide; last done.
+    setoid_rewrite Z.mul_comm; done. }
+  Unshelve. all: print_remaining_sidecond.
+Qed.
+End proof.
diff --git a/case_studies/minicell/src/evencell.rs b/case_studies/minicell/src/evencell.rs
new file mode 100644
index 0000000000000000000000000000000000000000..50b0b7fead70beab074945322dea42084618e345
--- /dev/null
+++ b/case_studies/minicell/src/evencell.rs
@@ -0,0 +1,32 @@
+
+#[repr(transparent)]
+#[rr::refined_by("()" : "unit")]
+#[rr::exists("x")]
+#[rr::invariant("Zeven x")]
+#[rr::mode(na)]
+pub struct EvenCell {
+    #[rr::field("x")]
+    value: i32,
+}
+
+impl EvenCell {
+    #[rr::requires("Zeven value")]
+    #[rr::returns("()")]
+    pub const fn new(value: i32) -> Self {
+        Self { value }
+    }
+
+    #[rr::exists("x")]
+    #[rr::ensures("Zeven x")]
+    #[rr::returns("x")]
+    pub fn into_inner(self) -> i32 {
+        self.value
+    }
+
+    #[rr::exists("x")]
+    #[rr::ensures("Zeven x")]
+    #[rr::returns("x")]
+    pub const fn get(&self) -> i32 {
+        self.value
+    }
+}
diff --git a/case_studies/minicell/src/example.rs b/case_studies/minicell/src/example.rs
index 4605516ce78b8c03bae6dcd5482bcfd359751120..ea54f3604fa6f23f9bc5fcf281f7243a8d58e5de 100644
--- a/case_studies/minicell/src/example.rs
+++ b/case_studies/minicell/src/example.rs
@@ -1,6 +1,6 @@
 use crate::Cell;
 
-#[rr::returns("()")]
+#[rr::verify]
 fn test1() {
     // pick invariant P := Zeven
     //#[rr::instantiate("Zeven")]
@@ -9,8 +9,7 @@ fn test1() {
     test2(&c);
 }
 
-#[rr::args("#Zeven")]
-#[rr::returns("()")]
+#[rr::args("Zeven")]
 fn test2(c: &Cell<i32>) {
     assert!(c.replace(2) % 2 == 0);
 }
diff --git a/case_studies/minicell/src/lib.rs b/case_studies/minicell/src/lib.rs
index 743d94b891ac032f77697b76b17f62fd8b065791..dbb017eff1e61d8aa4667f2ff0dd51e37a2aa256 100644
--- a/case_studies/minicell/src/lib.rs
+++ b/case_studies/minicell/src/lib.rs
@@ -6,6 +6,7 @@ use std::mem;
 use std::ptr;
 
 mod example;
+mod evencell;
 
 /* TODO:
  * 1. Add support for non-atomic invariants (na mode)
@@ -17,7 +18,6 @@ mod example;
 
 // We make UnsafeCell behave the same (in terms of refinements) as a value of T.
 #[repr(transparent)]
-// T_ty : type T_rt
 #[rr::refined_by("x" : "{rt_of T}")]
 pub struct UnsafeCell<T> {
     #[rr::field("x")]
@@ -25,25 +25,21 @@ pub struct UnsafeCell<T> {
 }
 
 impl<T> UnsafeCell<T> {
-    #[rr::params("x")]
-    #[rr::args("x")]
-    #[rr::returns("x")]
+    #[rr::returns("value")]
     pub const fn new(value: T) -> UnsafeCell<T> {
         UnsafeCell { value }
     }
 
-    #[rr::params("x")]
-    #[rr::args("x")]
-    #[rr::returns("x")]
+    #[rr::only_spec]
+    #[rr::returns("self")]
     pub fn into_inner(self) -> T {
         self.value
     }
 
-    #[rr::params("x")]
-    #[rr::args("(#x, γ)")]
+    #[rr::skip]
     #[rr::exists("γ'")]
-    #[rr::returns("(#x, γ')")]
-    #[rr::ensures(#iprop "inherit {'a} (Rel2 γ' γ eq)")]
+    #[rr::returns("(self.cur, γ')")]
+    #[rr::ensures(#iris "Inherit ulft_a InheritGhost (Rel2 γ' self.ghost (@eq (ty_xt T_ty → Prop)))")]
     pub fn get_mut<'a>(&'a mut self) -> &'a mut T {
         &mut self.value
     }
@@ -54,7 +50,8 @@ impl<T> UnsafeCell<T> {
     // which nice abstraction barriers are hard/annoying
     // Idea: add annotation to skip spec generation, at call sites add annotation in Coq code to inline.
     // Need new call-inline lemma
-    #[rr::inline]
+    //#[rr::inline]
+    #[rr::skip]
     pub const fn get(&self) -> *mut T {
         // TODO: we don't have repr(transparent) currently. We could change the code
         //
@@ -68,21 +65,19 @@ impl<T> UnsafeCell<T> {
     }
 }
 
-#[rr::refined_by("P" : "{rt_of T} → Prop")]
-#[rr::exists("x" : "{rt_of T}")]
-#[rr::invariant("P x")]
-// TODO: add support for this mode
-// #[rr::mode("na")]
+#[rr::refined_by("P" : "{rt_of T} → Prop" ; "{rt_of T} → Prop" )]
+#[rr::exists("x" : "{xt_of T}")]
+#[rr::invariant("P ($# x)")]
+#[rr::mode(na)]
 pub struct Cell<T> {
-    #[rr::field("x")]
+    #[rr::field("$# x")]
     value: UnsafeCell<T>,
 }
 
 impl<T> Cell<T> {
     // // NOTE: calling this function requires manual effort to instantiate P
-    #[rr::params("x" : "{rt_of T}", "P")]
-    #[rr::args("x")]
-    #[rr::requires("P x")]
+    #[rr::params("P")]
+    #[rr::requires("P ($# value)")]
     #[rr::returns("P")]
     pub const fn new(value: T) -> Cell<T> {
         Cell {
@@ -90,17 +85,15 @@ impl<T> Cell<T> {
         }
     }
 
-    #[rr::params("P", "x")]
-    #[rr::args("P", "x")]
-    #[rr::requires("P x")]
+    #[rr::only_spec]
+    #[rr::requires("self ($# val)")]
     pub fn set(&self, val: T) {
         let old = self.replace(val);
         drop(old);
     }
 
-    #[rr::params("P1", "P2")]
-    #[rr::args("#P1", "#P2")]
-    #[rr::requires("⌜∀ x, P1 x ↔ P2 x⌝")]
+    #[rr::only_spec]
+    #[rr::requires("∀ x, self (x) ↔ other (x)")]
     pub fn swap(&self, other: &Self) {
         // NOTE: will need to manually verify ptr::eq intrinsic
         if ptr::eq(self, other) {
@@ -115,10 +108,10 @@ impl<T> Cell<T> {
         }
     }
 
-    #[rr::args("#P", "x")]
-    #[rr::requires("P x")]
+    #[rr::only_spec]
+    #[rr::requires("self ($# val)")]
     #[rr::exists("y")]
-    #[rr::ensures("P y")]
+    #[rr::ensures("self ($# y)")]
     #[rr::returns("y")]
     pub fn replace(&self, val: T) -> T {
         // SAFETY: This can cause data races if called from a separate thread,
@@ -126,15 +119,16 @@ impl<T> Cell<T> {
         mem::replace(unsafe { &mut *self.value.get() }, val)
     }
 
-    #[rr::params("P")]
-    #[rr::args("P")]
+    // TODO: proof fails because we try to refold the (deinitialized) invariant
+    #[rr::only_spec]
     #[rr::exists("x")]
     #[rr::returns("x")]
-    #[rr::ensures("⌜P x⌝")]
+    #[rr::ensures("self ($# x)")]
     pub fn into_inner(self) -> T {
         self.value.into_inner()
     }
 
+    #[rr::skip]
     #[rr::params("P", "γ")]
     #[rr::args("(P, γ)")]
     #[rr::exists("x", "γ'")]
@@ -147,11 +141,10 @@ impl<T> Cell<T> {
 }
 
 impl<T: Copy> Cell<T> {
-    #[rr::params("P")]
-    #[rr::args("#P")]
+    #[rr::skip]
     #[rr::exists("x")]
     #[rr::returns("x")]
-    #[rr::ensures("⌜P x⌝")]
+    #[rr::ensures("self ($# x)")]
     pub fn get(&self) -> T {
         // SAFETY: This can cause data races if called from a separate thread,
         // but `Cell` is `!Sync` so this won't happen.
diff --git a/rr_frontend/radium/src/specs.rs b/rr_frontend/radium/src/specs.rs
index 924bb677481fde2df33c0930d10bc354fe9e150e..adff82b91b7473ac5e9c0419d49df436a7048202 100644
--- a/rr_frontend/radium/src/specs.rs
+++ b/rr_frontend/radium/src/specs.rs
@@ -955,12 +955,25 @@ impl InvariantSpec {
 
         // generate the spec definition
         let spec_name = format!("{}_inv_spec", self.type_name);
-        write!(
-            out,
-            "{indent}Program Definition {} : ex_inv_def ({}) ({}) := ",
-            spec_name, base_rfn_type, self.rfn_type,
-        )
-        .unwrap();
+
+        match self.flags {
+            InvariantSpecFlags::NonAtomic => {
+                write!(
+                    out,
+                    "{indent}Program Definition {} : na_ex_inv_def ({}) ({}) := ",
+                    spec_name, base_rfn_type, self.rfn_type,
+                )
+                .unwrap();
+            },
+            _ => {
+                write!(
+                    out,
+                    "{indent}Program Definition {} : ex_inv_def ({}) ({}) := ",
+                    spec_name, base_rfn_type, self.rfn_type,
+                )
+                .unwrap();
+            },
+        }
 
         match self.flags {
             InvariantSpecFlags::Persistent => {
@@ -1002,6 +1015,24 @@ impl InvariantSpec {
                 write!(out, "{indent}Next Obligation. ex_plain_t_solve_shr_mono. Qed.\n").unwrap();
                 write!(out, "{indent}Next Obligation. ex_plain_t_solve_shr. Qed.\n").unwrap();
             },
+            InvariantSpecFlags::NonAtomic => {
+                let own_inv = self.assemble_plain_owned_invariant();
+                let lft_outlives = self.assemble_ty_lfts();
+                let lft_wf_elctx = self.assemble_ty_wf_elctx();
+
+                write!(
+                    out,
+                    "na_mk_ex_inv_def\n\
+                    {indent}{indent}({})%type\n\
+                    {indent}{indent}({})\n\
+                    {indent}{indent}({own_inv})%I\n\
+                    {indent}{indent}({lft_outlives})\n\
+                    {indent}{indent}({lft_wf_elctx})\n\
+                    {indent}.\n",
+                    self.xt_type, self.xt_injection
+                )
+                .unwrap();
+            },
             _ => {
                 panic!("unimplemented invariant spec flag: {:?}", self.flags);
             },
@@ -1028,13 +1059,23 @@ impl InvariantSpec {
         write!(out, "{}", self.generate_coq_invariant_def(base_rfn_type)).unwrap();
 
         // generate the definition itself.
-        write!(
-            out,
-            "{indent}Definition {} : type ({}) :=\n\
-            {indent}{indent}ex_plain_t _ _ {spec_name} {}.\n",
-            self.type_name, self.rfn_type, base_type
-        )
-        .unwrap();
+        if InvariantSpecFlags::NonAtomic == self.flags {
+            write!(
+                out,
+                "{indent}Definition {} : type ({}) :=\n\
+                {indent}{indent}na_ex_plain_t _ _ {spec_name} {}.\n",
+                self.type_name, self.rfn_type, base_type
+            )
+            .unwrap();
+        } else {
+            write!(
+                out,
+                "{indent}Definition {} : type ({}) :=\n\
+                {indent}{indent}ex_plain_t _ _ {spec_name} {}.\n",
+                self.type_name, self.rfn_type, base_type
+            )
+            .unwrap();
+        }
         write!(out, "{indent}Global Typeclasses Transparent {}.\n", self.type_name).unwrap();
         write!(out, "{indent}Definition {}_rt : Type.\n", self.type_name).unwrap();
         write!(
diff --git a/theories/rust_typing/existentials_na_test.v b/theories/rust_typing/existentials_na_test.v
deleted file mode 100644
index fd6006fb0fbab6473303b6d423dee48f4d6c4159..0000000000000000000000000000000000000000
--- a/theories/rust_typing/existentials_na_test.v
+++ /dev/null
@@ -1,370 +0,0 @@
-(* NOTE: This file is expected to be deleted when the `rr_frontend` will be done. *)
-
-From refinedrust Require Import automation.
-From refinedrust Require Import existentials_na.
-From refinedrust Require Import typing.
-
-Section UnsafeCell_sls.
-  Context `{!refinedrustGS Σ}.
-
-  Definition UnsafeCell_sls : struct_layout_spec := mk_sls "UnsafeCell" [
-    ("value", IntSynType I32)] StructReprTransparent.
-  Definition UnsafeCell_st : syn_type := UnsafeCell_sls.
-End UnsafeCell_sls.
-
-Section Cell_sls.
-  Context `{!refinedrustGS Σ}.
-
-  Definition Cell_sls  : struct_layout_spec := mk_sls "Cell" [
-    ("value", UnsafeCell_st)] StructReprRust.
-  Definition Cell_st  : syn_type := Cell_sls .
-End Cell_sls.
-
-Section code.
-  Context `{!refinedrustGS Σ}.
-  Open Scope printing_sugar.
-
-  Definition UnsafeCell_new_def : function := {|
-    f_args := [
-      ("value", (it_layout I32) : layout)
-    ];
-    f_local_vars := [
-      ("__0", (use_layout_alg' (UnsafeCell_st)) : layout);
-      ("__2", (it_layout I32) : layout)
-    ];
-    f_code :=
-      <[
-      "_bb0" :=
-      "__2" <-{ IntOp I32 } use{ IntOp I32 } ("value");
-      "__0" <-{ (use_op_alg' (UnsafeCell_st)) } StructInit UnsafeCell_sls [("value", use{ IntOp I32 } ("__2") : expr)];
-      return (use{ (use_op_alg' (UnsafeCell_st)) } ("__0"))
-      ]>%E $
-      ∅;
-    f_init := "_bb0";
-  |}.
-
-  Definition UnsafeCell_into_inner_def : function := {|
-    f_args := [
-      ("self", (use_layout_alg' (UnsafeCell_st)) : layout)
-    ];
-    f_local_vars := [
-      ("__0", (it_layout I32) : layout)
-    ];
-    f_code :=
-      <[
-      "_bb0" :=
-      "__0" <-{ IntOp I32 } use{ IntOp I32 } (("self") at{ UnsafeCell_sls } "value");
-      return (use{ IntOp I32 } ("__0"))
-      ]>%E $
-      ∅;
-    f_init := "_bb0";
-  |}.
-
-  Definition UnsafeCell_get_old_def : function := {|
-    f_args := [
-      ("self", void* : layout)
-    ];
-    f_local_vars := [
-      ("__0", (it_layout I32) : layout)
-    ];
-    f_code :=
-      <[
-      "_bb0" :=
-      annot: CopyLftNameAnnot "plft3" "ulft__";
-      "__0" <-{ IntOp I32 } use{ IntOp I32 } ((!{ PtrOp } ( "self" )) at{ (UnsafeCell_sls) } "value");
-      return (use{ IntOp I32 } ("__0"))
-      ]>%E $
-      ∅;
-    f_init := "_bb0";
-  |}.
-
-  Definition UnsafeCell_get_def : function := {|
-    f_args := [
-      ("self", void* : layout)
-    ];
-    f_local_vars := [
-      ("__0", void* : layout);
-      ("__2", void* : layout);
-      ("__3", void* : layout)
-    ];
-    f_code :=
-      <[
-      "_bb0" :=
-      annot: CopyLftNameAnnot "plft3" "ulft_1";
-      "__3" <-{ PtrOp } &raw{ Shr } (!{ PtrOp } ( "self" ));
-      "__2" <-{ PtrOp } use{ PtrOp } ("__3");
-      "__0" <-{ PtrOp } use{ PtrOp } ("__2");
-      return (use{ PtrOp } ("__0"))
-      ]>%E $
-      ∅;
-    f_init := "_bb0";
-  |}.
-
-  Definition Cell_new_def (UnsafeCell_new_loc : loc) : function := {|
-    f_args := [
-      ("value", (it_layout I32) : layout)
-    ];
-    f_local_vars := [
-      ("__0", (use_layout_alg' (Cell_st)) : layout);
-      ("__2", (use_layout_alg' (UnsafeCell_st)) : layout);
-      ("__3", (it_layout I32) : layout)
-    ];
-    f_code :=
-      <[
-      "_bb0" :=
-      "__3" <-{ IntOp I32 } use{ IntOp I32 } ("value");
-      "__2" <-{ (use_op_alg' (UnsafeCell_st)) } CallE UnsafeCell_new_loc [] [] [@{expr} use{ IntOp I32 } ("__3")];
-      Goto "_bb1"
-      ]>%E $
-      <[
-      "_bb1" :=
-      "__0" <-{ (use_op_alg' (Cell_st)) } StructInit Cell_sls [("value", use{ (use_op_alg' (UnsafeCell_st)) } ("__2") : expr)];
-      return (use{ (use_op_alg' (Cell_st)) } ("__0"))
-      ]>%E $
-      ∅;
-    f_init := "_bb0";
-  |}.
-
-  Definition Cell_into_inner_def (UnsafeCell_into_inner_loc : loc) : function := {|
-    f_args := [
-      ("self", (use_layout_alg' (Cell_st)) : layout)
-    ];
-    f_local_vars := [
-      ("__0", (it_layout I32) : layout);
-      ("__2", (use_layout_alg' (UnsafeCell_st)) : layout)
-    ];
-    f_code :=
-      <[
-      "_bb0" :=
-      "__2" <-{ (use_op_alg' (UnsafeCell_st)) } use{ (use_op_alg' (UnsafeCell_st)) } (("self") at{ Cell_sls } "value");
-      "__0" <-{ IntOp I32 } CallE UnsafeCell_into_inner_loc [] [] [@{expr} use{ (use_op_alg' (UnsafeCell_st)) } ("__2")];
-      Goto "_bb1"
-      ]>%E $
-      <[
-      "_bb1" :=
-      return (use{ IntOp I32 } ("__0"))
-      ]>%E $
-      ∅;
-    f_init := "_bb0";
-  |}.
-End code.
-
-Section UnsafeCell_ty.
-  Context `{!refinedrustGS Σ}.
-
-  Definition UnsafeCell_ty : type (plist place_rfn [Z : Type]).
-  Proof using  Type*. exact (struct_t UnsafeCell_sls +[(int I32)]). Defined.
-
-  Definition UnsafeCell_rt : Type.
-  Proof using . let __a := eval hnf in (rt_of UnsafeCell_ty) in exact __a. Defined.
-
-  Global Typeclasses Transparent UnsafeCell_ty.
-  Global Typeclasses Transparent UnsafeCell_rt.
-End UnsafeCell_ty.
-Global Arguments UnsafeCell_rt : clear implicits.
-
-Section UnsafeCell_inv_t.
-  Context `{!refinedrustGS Σ}.
-
-  Program Definition UnsafeCell_inv_t_inv_spec : na_ex_inv_def (UnsafeCell_rt) (Z) :=
-    na_mk_ex_inv_def
-      ((Z)%type)
-      (xmap)
-      (λ π inner_rfn 'x, ⌜inner_rfn = -[#(x)]⌝ ∗ ⌜Zeven x⌝ ∗ True)%I
-      [] [].
-
-  Definition UnsafeCell_inv_t : type (Z) :=
-    na_ex_plain_t _ _ UnsafeCell_inv_t_inv_spec UnsafeCell_ty.
-
-  Definition UnsafeCell_inv_t_rt : Type.
-  Proof using. let __a := eval hnf in (rt_of UnsafeCell_inv_t) in exact __a. Defined.
-
-  Global Typeclasses Transparent UnsafeCell_inv_t.
-  Global Typeclasses Transparent UnsafeCell_inv_t_rt.
-End UnsafeCell_inv_t.
-Global Arguments UnsafeCell_inv_t_rt : clear implicits.
-
-Section Cell_ty.
-  Context `{!refinedrustGS Σ}.
-
-  Definition Cell_ty : type (plist place_rfn [UnsafeCell_inv_t_rt : Type]).
-  Proof using  Type*. exact (struct_t Cell_sls +[UnsafeCell_inv_t]). Defined.
-  Definition Cell_rt : Type.
-  Proof using . let __a := eval hnf in (rt_of Cell_ty) in exact __a. Defined.
-
-  Global Typeclasses Transparent Cell_ty.
-  Global Typeclasses Transparent Cell_rt.
-End Cell_ty.
-Global Arguments Cell_rt : clear implicits.
-
-Section Cell_inv_t.
-  Context `{!refinedrustGS Σ}.
-
-  Program Definition Cell_inv_t_inv_spec : na_ex_inv_def (Cell_rt) (Z) :=
-    na_mk_ex_inv_def
-      ((Z)%type)
-      (xmap)
-      (λ π inner_rfn 'x, ⌜inner_rfn = -[#(x)]⌝ ∗ ⌜Zeven x⌝ ∗ True)%I
-      [] [].
-
-  Definition Cell_inv_t : type (Z) :=
-    na_ex_plain_t _ _ Cell_inv_t_inv_spec Cell_ty.
-
-  Definition Cell_inv_t_rt : Type.
-  Proof using . let __a := eval hnf in (rt_of Cell_inv_t) in exact __a. Defined.
-
-  Global Typeclasses Transparent Cell_inv_t.
-  Global Typeclasses Transparent Cell_inv_t_rt.
-End Cell_inv_t.
-Global Arguments Cell_inv_t_rt : clear implicits.
-
-Section specs.
-  Context `{RRGS: !refinedrustGS Σ}.
-
-  Definition type_of_UnsafeCell_new  :=
-    fn(∀ ( *[]) : 0 | ( *[]): ([]) | (x) : (Z), (λ ϝ, []); x :@: (int I32); (λ π : thread_id, (⌜Zeven x⌝)))
-      → ∃ _ : unit, x @ UnsafeCell_inv_t; (λ π : thread_id, True).
-
-  Definition type_of_UnsafeCell_into_inner  :=
-    fn(∀ ( *[]) : 0 | ( *[]): ([]) | (x) : (Z), (λ ϝ, []); x :@: UnsafeCell_inv_t; (λ π : thread_id, True))
-      → ∃ _ : unit, x @ (int I32); (λ π : thread_id, (⌜Zeven x⌝)).
-
-  Definition type_of_UnsafeCell_get_old  :=
-    fn(∀ ( *[ulft_1]) : 1 | ( *[]) : ([]) | (x) : (_), (λ ϝ, []); x :@: (shr_ref ulft_1 UnsafeCell_inv_t); (λ π : thread_id, True))
-      → ∃ _ : unit, x @ (int I32); (λ π : thread_id, (⌜Zeven x⌝)).
-
-  Definition type_of_Cell_new  :=
-    fn(∀ ( *[]) : 0 | ( *[]) : [] | (x) : (Z), (λ ϝ, []); x :@: (int I32); (λ π : thread_id, (⌜Zeven x⌝)))
-      → ∃ _ : unit, x @ Cell_inv_t; (λ π : thread_id, True).
-
-  Definition type_of_Cell_into_inner  :=
-    fn(∀ ( *[]) : 0 | ( *[]) : [] | (x) : (_), (λ ϝ, []); x :@: Cell_inv_t; (λ π : thread_id, True))
-      → ∃ _ : unit, x @ (int I32); (λ π : thread_id, (⌜Zeven x⌝)).
-End specs.
-
-Section proof.
-  Context `{RRGS: !refinedrustGS Σ}.
-
-  Definition UnsafeCell_new_lemma (Ï€ : thread_id) : Prop :=
-    syn_type_is_layoutable ((UnsafeCell_sls : syn_type)) →
-    ⊢ typed_function π (UnsafeCell_new_def ) [UnsafeCell_st; IntSynType I32] (<tag_type> type_of_UnsafeCell_new ).
-
-  Definition UnsafeCell_into_inner_lemma (Ï€ : thread_id) : Prop :=
-    syn_type_is_layoutable ((UnsafeCell_sls : syn_type)) →
-    ⊢ typed_function π (UnsafeCell_into_inner_def ) [IntSynType I32] (<tag_type> type_of_UnsafeCell_into_inner ).
-
-  Definition UnsafeCell_get_old_lemma (Ï€ : thread_id) : Prop :=
-    syn_type_is_layoutable (Cell_st) →
-    ⊢ typed_function π (UnsafeCell_get_old_def ) [IntSynType I32] (<tag_type> type_of_UnsafeCell_get_old ).
-
-  Definition Cell_new_lemma (Ï€ : thread_id) : Prop :=
-    ∀ (UnsafeCell_new_loc : loc) ,
-    syn_type_is_layoutable ((UnsafeCell_sls : syn_type)) →
-    syn_type_is_layoutable ((Cell_sls : syn_type)) →
-    UnsafeCell_new_loc ◁ᵥ{π} UnsafeCell_new_loc @ function_ptr [IntSynType I32] (<tag_type> spec! ( *[]) : 0 | ( *[]) : ([]), type_of_UnsafeCell_new (RRGS := RRGS) <MERGE!>) -∗
-    typed_function π (Cell_new_def UnsafeCell_new_loc  ) [Cell_st; UnsafeCell_st; IntSynType I32] (<tag_type> type_of_Cell_new ).
-End proof.
-
-Ltac UnsafeCell_new_prelude :=
-  unfold UnsafeCell_new_lemma;
-  set (FN_NAME := FUNCTION_NAME "UnsafeCell_new");
-  intros;
-  iStartProof;
-  let ϝ := fresh "ϝ" in
-  start_function "UnsafeCell_new" ϝ ( [] ) ( [] ) (  x ) (  x );
-  set (loop_map := BB_INV_MAP (PolyNil));
-  intros arg_value local___0 local___2;
-  init_lfts (named_lft_update "_flft" ϝ $ ∅ );
-  init_tyvars ( ∅ ).
-
-Ltac UnsafeCell_into_inner_prelude :=
-  unfold UnsafeCell_into_inner_lemma;
-  set (FN_NAME := FUNCTION_NAME "UnsafeCell_into_inner");
-  intros;
-  iStartProof;
-  let ϝ := fresh "ϝ" in
-  start_function "UnsafeCell_into_inner" ϝ ( [] ) ( [] ) (  x ) (  x );
-  set (loop_map := BB_INV_MAP (PolyNil));
-  intros arg_self local___0;
-  init_lfts (named_lft_update "_flft" ϝ $ ∅ );
-  init_tyvars ( ∅ ).
-
-Ltac UnsafeCell_get_old_prelude :=
-  unfold UnsafeCell_get_old_lemma;
-  set (FN_NAME := FUNCTION_NAME "Cell_get");
-  intros;
-  iStartProof;
-  let ϝ := fresh "ϝ" in
-  let ulft__ := fresh "ulft__" in
-  start_function "UnsafeCell_get_old" ϝ ( [ ulft__ [] ] ) ( [] ) (  x ) (  x );
-  set (loop_map := BB_INV_MAP (PolyNil));
-  intros arg_self local___0;
-  init_lfts (named_lft_update "ulft__" ulft__ $ named_lft_update "_flft" ϝ $ ∅ );
-  init_tyvars ( ∅ ).
-
-Ltac Cell_new_prelude :=
-  unfold Cell_new_lemma;
-  set (FN_NAME := FUNCTION_NAME "Cell_new");
-  intros;
-  iStartProof;
-  let ϝ := fresh "ϝ" in
-  start_function "Cell_T_new" ϝ ( [] ) ( [] ) (  x ) (  x );
-  set (loop_map := BB_INV_MAP (PolyNil));
-  intros arg_value local___0 local___2 local___3;
-  init_lfts (named_lft_update "_flft" ϝ $ ∅ );
-  init_tyvars ( ∅ ).
-
-Section proof.
-  Context `{!refinedrustGS Σ}.
-
-  Lemma UnsafeCell_new_proof (Ï€ : thread_id) :
-    UnsafeCell_new_lemma π.
-  Proof.
-    UnsafeCell_new_prelude.
-
-    repeat liRStep; liShow.
-
-    all: print_remaining_goal.
-    Unshelve. all: sidecond_solver.
-    Unshelve. all: sidecond_hammer.
-    Unshelve. all: print_remaining_sidecond.
-  Qed.
-
-  Lemma UnsafeCell_into_inner_proof (Ï€ : thread_id) :
-    UnsafeCell_into_inner_lemma π.
-  Proof.
-    UnsafeCell_into_inner_prelude.
-
-    repeat liRStep; liShow.
-
-    all: print_remaining_goal.
-    Unshelve. all: sidecond_solver.
-    Unshelve. all: sidecond_hammer.
-    Unshelve. all: print_remaining_sidecond.
-  Qed.
-
-  Lemma Cell_new_proof (Ï€ : thread_id) :
-    Cell_new_lemma π.
-  Proof.
-    Cell_new_prelude.
-
-    repeat liRStep; liShow.
-
-    all: print_remaining_goal.
-    Unshelve. all: sidecond_solver.
-    Unshelve. all: sidecond_hammer.
-    Unshelve. all: print_remaining_sidecond.
-  Qed.
-
-  Lemma UnsafeCell_get_old_proof (Ï€ : thread_id) :
-    UnsafeCell_get_old_lemma π.
-  Proof.
-    UnsafeCell_get_old_prelude.
-
-    repeat liRStep; liShow.
-
-    Unshelve. all: sidecond_solver.
-    Unshelve. all: sidecond_hammer.
-    Unshelve. all: print_remaining_sidecond.
-  Qed.
-End proof.
diff --git a/theories/rust_typing/typing.v b/theories/rust_typing/typing.v
index a5044638c74d36dc4f51b0ec744b0abb4dab57f2..46f89021900211f6e1a3502d09f41501a5ff95a8 100644
--- a/theories/rust_typing/typing.v
+++ b/theories/rust_typing/typing.v
@@ -1,4 +1,4 @@
-From refinedrust Require Export static type program_rules int int_rules products mut_ref shr_ref functions uninit box programs enum maybe_uninit alias_ptr fixpoint existentials arrays value generics xmap.
+From refinedrust Require Export static type program_rules int int_rules products mut_ref shr_ref functions uninit box programs enum maybe_uninit alias_ptr fixpoint existentials existentials_na arrays value generics xmap.
 From refinedrust Require Export automation.loc_eq manual automation.
 From refinedrust Require Export simpl.