diff --git a/README.md b/README.md
index 6ab8341d85462026f92cc7c9f0c754ec8ce1b570..e2f729efff941867e6e94fd5ffffc9852da193cd 100644
--- a/README.md
+++ b/README.md
@@ -88,10 +88,11 @@ These include:
 | `dump_borrowck_info` | Boolean | Dumps borrowck debug output in the log directory |
 | `output_dir` | Relative/absolute path | Determines the directory where the generated output files will be placed |
 | `log_dir` | Relative/absolute path | Determines the directory where logs and debug dumps will be placed if enabled |
-| `shims` | Relative path | Determines the JSON file storing information about shims that RefinedRust uses |
+| `shims` | Relative/absolute path | Determines the JSON file storing information about shims that RefinedRust uses |
 | `run_check` | Boolean | Automatically call the Coq type checker on the generated files |
 | `verify_deps` | Boolean | Verify dependencies or not |
 | `admit_proofs` | Boolean | Skip Coq's `Qed` check and instead run `Admitted` |
+| `extra_specs` | Relative/absolute path | File whose contents will be inlined at the end of the generated specs file |
 
 The path to the config file can also be specified via the environment variable `RR_CONFIG`.
 Setting this variable will also change the `work_dir` (relative to which paths are interpreted) to the path of `RR_CONFIG`.
diff --git a/rr_frontend/rrconfig/src/lib.rs b/rr_frontend/rrconfig/src/lib.rs
index d544ea21f26ee93ed9efd7963b08b93d5b0d031a..80ac0bedd024cfc2cadfc979d611479e24f118cd 100644
--- a/rr_frontend/rrconfig/src/lib.rs
+++ b/rr_frontend/rrconfig/src/lib.rs
@@ -82,7 +82,7 @@ pub fn dump() -> String {
 /// Makes the path absolute with respect to the work_dir.
 fn make_path_absolute(path: &str) -> PathBuf {
     // read the base path we set
-    let base_path: String = work_dir(); 
+    let base_path: String = work_dir();
 
     let path_buf = std::path::PathBuf::from(path);
     if path_buf.is_absolute() {
@@ -160,7 +160,7 @@ pub fn output_dir() -> Option<PathBuf> {
     read_optional_setting("output_dir").map(|s: String| make_path_absolute(&s))
 }
 
-/// Whether to admit proofs of functions instead of running Qed. 
+/// Whether to admit proofs of functions instead of running Qed.
 pub fn admit_proofs() -> bool {
     read_setting("admit_proofs")
 }
@@ -170,6 +170,11 @@ pub fn shim_file() -> Option<PathBuf> {
     read_optional_setting("shims").map(|s: String| make_path_absolute(&s))
 }
 
+/// Which file should we read extra specs from?
+pub fn extra_specs_file() -> Option<PathBuf> {
+    read_optional_setting("extra_specs").map(|s: String| make_path_absolute(&s))
+}
+
 /// Run the proof checker after generating the Coq code?
 pub fn check_proofs() -> bool {
     read_setting("run_check")
diff --git a/rr_frontend/translation/src/lib.rs b/rr_frontend/translation/src/lib.rs
index 5eb1091138b5a9c797723b0374d9425b9248d685..b3a42dad9eedee3601b8a3a4ae4eb48069f8021f 100644
--- a/rr_frontend/translation/src/lib.rs
+++ b/rr_frontend/translation/src/lib.rs
@@ -36,7 +36,7 @@ use rustc_middle::ty as ty;
 use rustc_middle::ty::TyCtxt;
 
 use std::fs;
-use std::io::{self, Write};
+use std::io::{self, Write, Read};
 use std::path::Path;
 
 use typed_arena::Arena;
@@ -290,6 +290,17 @@ impl<'tcx, 'rcx> VerificationCtxt<'tcx, 'rcx> {
             }
         }
 
+        // Include extra specs
+        if let Some(extra_specs_path) = rrconfig::extra_specs_file() {
+            writeln!(spec_file, "(* Included specifications from configured file {:?} *)", extra_specs_path).unwrap();
+            let mut extra_specs_file = io::BufReader::new(fs::File::open(extra_specs_path).unwrap());
+
+            let mut extra_specs_string = String::new();
+            extra_specs_file.read_to_string(&mut extra_specs_string).unwrap();
+
+            write!(spec_file, "{}", extra_specs_string).unwrap();
+        }
+
         spec_file.write("End specs.".as_bytes()).unwrap();
     }
 
diff --git a/theories/rust_typing/automation.v b/theories/rust_typing/automation.v
index 9315ea8aac724d2b98f8c8e85cbfb433cb28736e..07f6eed328cac09e369e2ad4acaa477421823fb2 100644
--- a/theories/rust_typing/automation.v
+++ b/theories/rust_typing/automation.v
@@ -876,123 +876,14 @@ Ltac sidecond_hook ::=
   | |- ty_allows_writes _ =>
       solve_ty_allows
   | |- _ =>
-      try solve [solve_layout_size | solve_layout_eq | solve_op_alg];
-      try solve_layout_alg
+      try solve_layout_alg;
+      try solve_op_alg;
+      try solve_layout_eq
+      (*try solve [solve_layout_size | solve_layout_eq | solve_op_alg];*)
+      (*try solve_layout_alg*)
   end.
 
 
-(** ** Proofmode support for manual proofs *)
-Lemma tac_typed_val_expr_bind' `{!typeGS Σ} π E L K e T :
-  typed_val_expr π E L (W.to_expr e) (λ L' v rt ty r,
-    v ◁ᵥ{π} r @ ty -∗ typed_val_expr π E L' (W.to_expr (W.fill K (W.Val v))) T) -∗
-  typed_val_expr π E L (W.to_expr (W.fill K e)) T.
-Proof.
-  iIntros "He".
-  rewrite /typed_val_expr.
-  iIntros (Φ) "#CTX #HE HL Hna Hcont".
-  iApply tac_wp_bind'.
-  iApply ("He" with "CTX HE HL Hna").
-  iIntros (L' v rt ty r) "HL Hna Hv Hcont'".
-  iApply ("Hcont'" with "Hv CTX HE HL Hna"). done.
-Qed.
-Lemma tac_typed_val_expr_bind `{!typeGS Σ} π E L e Ks e' T :
-  W.find_expr_fill e false = Some (Ks, e') →
-  typed_val_expr π E L (W.to_expr e') (λ L' v rt ty r,
-    if Ks is [] then T L' v rt ty r else
-      v ◁ᵥ{π} r @ ty -∗ typed_val_expr π E L' (W.to_expr (W.fill Ks (W.Val v))) T) -∗
-  typed_val_expr π E L (W.to_expr e) T.
-Proof.
-  move => /W.find_expr_fill_correct ->. move: Ks => [|K Ks] //.
-  { auto. }
-  move: (K::Ks) => {K}Ks. by iApply tac_typed_val_expr_bind'.
-Qed.
-
-Tactic Notation "typed_val_expr_bind" :=
-  iStartProof;
-  lazymatch goal with
-  | |- envs_entails _ (typed_val_expr ?Ï€ ?E ?L ?e ?T) =>
-    let e' := W.of_expr e in change (typed_val_expr π E L e T) with (typed_val_expr π E L (W.to_expr e') T);
-    iApply tac_typed_val_expr_bind; [done |];
-    unfold W.to_expr; simpl
-  | _ => fail "typed_val_expr_bind: not a 'typed_val_expr'"
-  end.
-
-Lemma fupd_typed_val_expr `{!typeGS Σ} π E L e T :
-  (|={⊤}=> typed_val_expr π E L e T) -∗ typed_val_expr π E L e T.
-Proof.
-  rewrite /typed_val_expr.
-  iIntros "HT" (?) "CTX HE HL Hna Hc".
-  iApply fupd_wp. iMod ("HT") as "HT". iApply ("HT" with "CTX HE HL Hna Hc").
-Qed.
-Lemma fupd_typed_call `{!typeGS Σ} π E L κs v (P : iProp Σ) vl tys T :
-  (|={⊤}=> typed_call π E L κs v P vl tys T) -∗ typed_call π E L κs v P vl tys T.
-Proof.
-  rewrite /typed_call.
-  iIntros "HT HP Ha".
-  iApply fupd_typed_val_expr. iMod "HT" as "HT". iApply ("HT" with "HP Ha").
-Qed.
-
-
-Lemma tac_typed_stmt_bind `{!typeGS Σ} π E L s e Ks fn ϝ T :
-  W.find_stmt_fill s = Some (Ks, e) →
-  typed_val_expr π E L (W.to_expr e) (λ L' v rt ty r,
-    v ◁ᵥ{π} r @ ty -∗ typed_stmt π E L' (W.to_stmt (W.stmt_fill Ks (W.Val v))) fn T ϝ) -∗
-  typed_stmt π E L (W.to_stmt s) fn T ϝ.
-Proof.
-  move => /W.find_stmt_fill_correct ->. iIntros "He".
-  rewrite /typed_stmt.
-  iIntros (?) "#CTX #HE HL Hna Hcont".
-  rewrite stmt_wp_eq. iIntros (? rf ?) "?".
-  have [Ks' HKs']:= W.stmt_fill_correct Ks rf. rewrite HKs'.
-  iApply wp_bind.
-  iApply (wp_wand with "[Hna He HL]").
-  { rewrite /typed_val_expr. iApply ("He" with "CTX HE HL Hna").
-    iIntros (L' v rt ty r) "HL Hna Hv Hcont".
-    iApply ("Hcont" with "Hv CTX HE HL Hna"). }
-  iIntros (v) "HWP".
-  rewrite -(HKs' (W.Val _)) /W.to_expr.
-  iSpecialize ("HWP" with "Hcont").
-  rewrite stmt_wp_eq/stmt_wp_def/=.
-  iApply "HWP"; done.
-Qed.
-
-Tactic Notation "typed_stmt_bind" :=
-  iStartProof;
-  lazymatch goal with
-  | |- envs_entails _ (typed_stmt ?π ?E ?L ?s ?fn ?R ?ϝ) =>
-    let s' := W.of_stmt s in change (typed_stmt π E L s fn R ϝ) with (typed_stmt π E L (W.to_stmt s') fn R ϝ);
-    iApply tac_typed_stmt_bind; [done |];
-    unfold W.to_expr, W.to_stmt; simpl; unfold W.to_expr; simpl
-  | _ => fail "typed_stmt_bind: not a 'typed_stmt'"
-  end.
-
-Lemma intro_typed_stmt `{!typeGS Σ} fn R ϝ π E L s Φ :
-  rrust_ctx -∗
-  elctx_interp E -∗
-  llctx_interp L -∗
-  na_own π shrE -∗
-  (∀ (L' : llctx) (v : val), llctx_interp L' -∗ na_own π shrE -∗ ([∗ list] l ∈ rf_locs fn, l.1 ↦|l.2|) -∗ R v L' -∗ Φ v) -∗
-  typed_stmt π E L s fn R ϝ -∗
-  WPs s {{ f_code (rf_fn fn), Φ }}.
-Proof.
-  iIntros "#CTX #HE HL Hna Hcont Hs".
-  rewrite /typed_stmt.
-  iApply ("Hs" with "CTX HE HL Hna Hcont").
-Qed.
-Lemma fupd_typed_stmt `{!typeGS Σ} π E L s rf R ϝ :
-  ⊢ (|={⊤}=> typed_stmt π E L s rf R ϝ) -∗ typed_stmt π E L s rf R ϝ.
-Proof.
-  iIntros "HT". rewrite /typed_stmt. iIntros (?) "CTX HE HL Hna Hcont".
-  iMod ("HT") as "HT". iApply ("HT" with "CTX HE HL Hna Hcont").
-Qed.
-
-Ltac to_typed_stmt SPEC :=
-  iStartProof;
-  lazymatch goal with
-  | FN : runtime_function |- envs_entails _ (WPs ?s {{ ?code, ?c }}) =>
-    iApply (intro_typed_stmt FN with SPEC)
-  end.
-
 (** ** Hints for automation *)
 Global Hint Extern 0 (LayoutSizeEq _ _) => rewrite /LayoutSizeEq; solve_layout_size : typeclass_instances.
 Global Hint Extern 0 (LayoutSizeLe _ _) => rewrite /LayoutSizeLe; solve_layout_size : typeclass_instances.
diff --git a/theories/rust_typing/manual.v b/theories/rust_typing/manual.v
new file mode 100644
index 0000000000000000000000000000000000000000..94701bd731c34b013fe9847b5ed236937e70de69
--- /dev/null
+++ b/theories/rust_typing/manual.v
@@ -0,0 +1,258 @@
+From iris.proofmode Require Import coq_tactics reduction string_ident.
+From refinedrust Require Import programs arrays automation.
+
+
+(** * Proofmode support for manual proofs *)
+
+Section updateable.
+  Context `{!typeGS Σ}.
+
+  Definition updateable (π : thread_id) (E : elctx) (L : llctx) (T : llctx → iProp Σ) : iProp Σ :=
+    rrust_ctx -∗
+    elctx_interp E -∗
+    llctx_interp L -∗
+    na_own π shrE ={⊤}=∗
+    ∃ L2, llctx_interp L2 ∗ na_own π shrE ∗ T L2.
+  Class Updateable (P : iProp Σ) := {
+    updateable_E : elctx;
+    updateable_L : llctx;
+    updateable_Ï€ : thread_id;
+    updateable_core : thread_id → elctx → llctx → iProp Σ;
+    updateable_prove π E L : updateable π E L (λ L2, updateable_core π E L2) -∗ updateable_core π E L;
+    updateable_eq : updateable_core updateable_π updateable_E updateable_L ⊣⊢ P
+  }.
+
+  Lemma updateable_mono π E L T1 T2 :
+    updateable π E L T1 -∗
+    (∀ L, T1 L -∗ T2 L) -∗
+    updateable π E L T2.
+  Proof.
+    iIntros "HT Hw".
+    iIntros "#CTX #HE HL Hna".
+    iMod ("HT" with "CTX HE HL Hna") as "(%L2 & HL & Hna & HT)".
+    iSpecialize ("Hw" with "HT").
+    iExists L2. by iFrame.
+  Qed.
+  Lemma updateable_intro π E L T :
+    T L ⊢ updateable π E L T.
+  Proof.
+    iIntros "HT #CTX HE HL Hna".
+    iExists L. by iFrame.
+  Qed.
+
+  Lemma add_updateable P `{!Updateable P} :
+    updateable updateable_π updateable_E updateable_L (λ L2, updateable_core updateable_π  updateable_E L2) -∗ P.
+  Proof.
+    iIntros "HT".
+    iApply updateable_eq.
+    iApply updateable_prove.
+    iApply (updateable_mono with "HT").
+    eauto.
+  Qed.
+
+  Global Program Instance updateable_typed_val_expr π E L e T :
+    Updateable (typed_val_expr π E L e T) := {|
+      updateable_E := E;
+      updateable_L := L;
+      updateable_π := π;
+      updateable_core π E L := typed_val_expr π E L e T;
+  |}.
+  Next Obligation.
+    iIntros (_ _ _ e T π E L).
+    rewrite /typed_val_expr.
+    iIntros "HT" (?) "#CTX #HE HL Hna Hc".
+    iApply fupd_wp. iMod ("HT" with "CTX HE HL Hna") as "(%L2 & HL & Hna & HT)".
+    iApply ("HT" with "CTX HE HL Hna Hc").
+  Qed.
+  Next Obligation.
+    simpl. eauto.
+  Qed.
+
+  Global Program Instance updateable_typed_call π E L κs v (P : iProp Σ) vl tys T :
+    Updateable (typed_call π E L κs v P vl tys T) := {|
+      updateable_E := E;
+      updateable_L := L;
+      updateable_π := π;
+      updateable_core π E L := typed_call π E L κs v P vl tys T;
+  |}.
+  Next Obligation.
+    iIntros (_ _ _ ? ? ? ? ? ? π E L).
+    rewrite /typed_call.
+    iIntros "HT HP Ha".
+    unshelve iApply add_updateable; first apply _.
+    iApply (updateable_mono with "HT").
+    iIntros (L2) "Hb".
+    iApply ("Hb" with "HP Ha").
+  Qed.
+  Next Obligation.
+    simpl. eauto.
+  Qed.
+
+
+  Global Program Instance updateable_typed_stmt π E L s rf R ϝ :
+    Updateable (typed_stmt π E L s rf R ϝ) := {|
+      updateable_E := E;
+      updateable_L := L;
+      updateable_π := π;
+      updateable_core π E L := typed_stmt π E L s rf R ϝ;
+  |}.
+  Next Obligation.
+    iIntros (_ _ _ ? ? ? ? π E L).
+    iIntros "HT". rewrite /typed_stmt.
+    iIntros (?) "#CTX #HE HL Hna Hcont".
+    iMod ("HT" with "CTX HE HL Hna") as "(%L2 & HL & Hna & HT)".
+    iApply ("HT" with "CTX HE HL Hna Hcont").
+  Qed.
+  Next Obligation.
+    simpl. eauto.
+  Qed.
+
+  Lemma fupd_typed_val_expr `{!typeGS Σ} π E L e T :
+    (|={⊤}=> typed_val_expr π E L e T) -∗ typed_val_expr π E L e T.
+  Proof.
+    rewrite /typed_val_expr.
+    iIntros "HT" (?) "CTX HE HL Hna Hc".
+    iApply fupd_wp. iMod ("HT") as "HT". iApply ("HT" with "CTX HE HL Hna Hc").
+  Qed.
+  Lemma fupd_typed_call `{!typeGS Σ} π E L κs v (P : iProp Σ) vl tys T :
+    (|={⊤}=> typed_call π E L κs v P vl tys T) -∗ typed_call π E L κs v P vl tys T.
+  Proof.
+    rewrite /typed_call.
+    iIntros "HT HP Ha".
+    iApply fupd_typed_val_expr. iMod "HT" as "HT". iApply ("HT" with "HP Ha").
+  Qed.
+
+  Lemma fupd_typed_stmt `{!typeGS Σ} π E L s rf R ϝ :
+    ⊢ (|={⊤}=> typed_stmt π E L s rf R ϝ) -∗ typed_stmt π E L s rf R ϝ.
+  Proof.
+    iIntros "HT". rewrite /typed_stmt. iIntros (?) "CTX HE HL Hna Hcont".
+    iMod ("HT") as "HT". iApply ("HT" with "CTX HE HL Hna Hcont").
+  Qed.
+End updateable.
+
+Section updateable_rules.
+  Context `{!typeGS Σ}.
+
+  Lemma updateable_typed_array_access l off st π E L T :
+    find_in_context (FindLoc l π)  (λ '(existT _ (lt, r, k)),
+      typed_array_access π E L l off st lt r k (λ L2 rt2 ty2 len2 iml2 rs2 k2 rte lte re,
+        l ◁ₗ[π, k2] #rs2 @ ArrayLtype ty2 len2 iml2 -∗
+        (l offsetst{st}ₗ off) ◁ₗ[π, k2] re @ lte -∗
+        updateable π E L2 T)) -∗
+    updateable π E L T.
+  Proof.
+    iIntros "HT #CTX #HE HL Hna".
+    rewrite /FindLoc /find_in_context/=.
+    iDestruct "HT" as ([rt [[lt r] k]]) "(Ha & Hb)".
+    rewrite /typed_array_access.
+    iMod ("Hb" with "[] [] CTX HE HL Ha") as "(%L2 & %k2 & %rt2 & %ty2 & %len & %iml & %rs2 & %rte & %re & %lte & Hl & He & HL & HT)";
+    [set_solver.. | ].
+    iPoseProof ("HT" with "Hl He") as "Ha".
+    iApply ("Ha" with "CTX HE HL").
+    iFrame.
+  Qed.
+
+  (* TODO: add lemma for unfolding / subtyping? *)
+End updateable_rules.
+
+Ltac add_updateable :=
+  match goal with
+  | |- envs_entails _ ?P =>
+      unshelve notypeclasses refine (tac_fast_apply (add_updateable P) _);
+      [ apply _ | apply _ | ]
+  end.
+
+
+
+
+
+
+
+Lemma tac_typed_val_expr_bind' `{!typeGS Σ} π E L K e T :
+  typed_val_expr π E L (W.to_expr e) (λ L' v rt ty r,
+    v ◁ᵥ{π} r @ ty -∗ typed_val_expr π E L' (W.to_expr (W.fill K (W.Val v))) T) -∗
+  typed_val_expr π E L (W.to_expr (W.fill K e)) T.
+Proof.
+  iIntros "He".
+  rewrite /typed_val_expr.
+  iIntros (Φ) "#CTX #HE HL Hna Hcont".
+  iApply tac_wp_bind'.
+  iApply ("He" with "CTX HE HL Hna").
+  iIntros (L' v rt ty r) "HL Hna Hv Hcont'".
+  iApply ("Hcont'" with "Hv CTX HE HL Hna"). done.
+Qed.
+Lemma tac_typed_val_expr_bind `{!typeGS Σ} π E L e Ks e' T :
+  W.find_expr_fill e false = Some (Ks, e') →
+  typed_val_expr π E L (W.to_expr e') (λ L' v rt ty r,
+    if Ks is [] then T L' v rt ty r else
+      v ◁ᵥ{π} r @ ty -∗ typed_val_expr π E L' (W.to_expr (W.fill Ks (W.Val v))) T) -∗
+  typed_val_expr π E L (W.to_expr e) T.
+Proof.
+  move => /W.find_expr_fill_correct ->. move: Ks => [|K Ks] //.
+  { auto. }
+  move: (K::Ks) => {K}Ks. by iApply tac_typed_val_expr_bind'.
+Qed.
+
+Tactic Notation "typed_val_expr_bind" :=
+  iStartProof;
+  lazymatch goal with
+  | |- envs_entails _ (typed_val_expr ?Ï€ ?E ?L ?e ?T) =>
+    let e' := W.of_expr e in change (typed_val_expr π E L e T) with (typed_val_expr π E L (W.to_expr e') T);
+    iApply tac_typed_val_expr_bind; [done |];
+    unfold W.to_expr; simpl
+  | _ => fail "typed_val_expr_bind: not a 'typed_val_expr'"
+  end.
+
+Lemma tac_typed_stmt_bind `{!typeGS Σ} π E L s e Ks fn ϝ T :
+  W.find_stmt_fill s = Some (Ks, e) →
+  typed_val_expr π E L (W.to_expr e) (λ L' v rt ty r,
+    v ◁ᵥ{π} r @ ty -∗ typed_stmt π E L' (W.to_stmt (W.stmt_fill Ks (W.Val v))) fn T ϝ) -∗
+  typed_stmt π E L (W.to_stmt s) fn T ϝ.
+Proof.
+  move => /W.find_stmt_fill_correct ->. iIntros "He".
+  rewrite /typed_stmt.
+  iIntros (?) "#CTX #HE HL Hna Hcont".
+  rewrite stmt_wp_eq. iIntros (? rf ?) "?".
+  have [Ks' HKs']:= W.stmt_fill_correct Ks rf. rewrite HKs'.
+  iApply wp_bind.
+  iApply (wp_wand with "[Hna He HL]").
+  { rewrite /typed_val_expr. iApply ("He" with "CTX HE HL Hna").
+    iIntros (L' v rt ty r) "HL Hna Hv Hcont".
+    iApply ("Hcont" with "Hv CTX HE HL Hna"). }
+  iIntros (v) "HWP".
+  rewrite -(HKs' (W.Val _)) /W.to_expr.
+  iSpecialize ("HWP" with "Hcont").
+  rewrite stmt_wp_eq/stmt_wp_def/=.
+  iApply "HWP"; done.
+Qed.
+
+Tactic Notation "typed_stmt_bind" :=
+  iStartProof;
+  lazymatch goal with
+  | |- envs_entails _ (typed_stmt ?π ?E ?L ?s ?fn ?R ?ϝ) =>
+    let s' := W.of_stmt s in change (typed_stmt π E L s fn R ϝ) with (typed_stmt π E L (W.to_stmt s') fn R ϝ);
+    iApply tac_typed_stmt_bind; [done |];
+    unfold W.to_expr, W.to_stmt; simpl; unfold W.to_expr; simpl
+  | _ => fail "typed_stmt_bind: not a 'typed_stmt'"
+  end.
+
+Lemma intro_typed_stmt `{!typeGS Σ} fn R ϝ π E L s Φ :
+  rrust_ctx -∗
+  elctx_interp E -∗
+  llctx_interp L -∗
+  na_own π shrE -∗
+  (∀ (L' : llctx) (v : val), llctx_interp L' -∗ na_own π shrE -∗ ([∗ list] l ∈ rf_locs fn, l.1 ↦|l.2|) -∗ R v L' -∗ Φ v) -∗
+  typed_stmt π E L s fn R ϝ -∗
+  WPs s {{ f_code (rf_fn fn), Φ }}.
+Proof.
+  iIntros "#CTX #HE HL Hna Hcont Hs".
+  rewrite /typed_stmt.
+  iApply ("Hs" with "CTX HE HL Hna Hcont").
+Qed.
+
+Ltac to_typed_stmt SPEC :=
+  iStartProof;
+  lazymatch goal with
+  | FN : runtime_function |- envs_entails _ (WPs ?s {{ ?code, ?c }}) =>
+    iApply (intro_typed_stmt FN with SPEC)
+  end.
diff --git a/theories/rust_typing/typing.v b/theories/rust_typing/typing.v
index 186b423414ce757083b65c5f6b7bcbae68ae5418..b81917485e7787943fd774483d69624dff87f3ee 100644
--- a/theories/rust_typing/typing.v
+++ b/theories/rust_typing/typing.v
@@ -1,5 +1,5 @@
 From refinedrust Require Export type program_rules int int_rules products references functions uninit box programs enum maybe_uninit alias_ptr existentials arrays value.
-From refinedrust Require Export automation.
+From refinedrust Require Export manual automation.
 
 Global Open Scope Z_scope.