diff --git a/theories/typing/bool.v b/theories/typing/bool.v
index fd4c8c7b8dcee92f7c25a2fec285bb70b895320e..eed4fec3b1e3c4bae05f8557f5b94d619e1fa6e9 100644
--- a/theories/typing/bool.v
+++ b/theories/typing/bool.v
@@ -32,22 +32,20 @@ Section typing.
 
   Lemma type_bool (b : Datatypes.bool) E L C T x e :
     Closed (x :b: []) e →
-    (∀ (v : val), typed_body E L C ((v ◁ bool) :: T) (subst' x v e)) →
+    (∀ (v : val), typed_body E L C ((v ◁ bool) :: T) (subst' x v e)) -∗
     typed_body E L C T (let: x := #b in e).
-  Proof.
-    intros. eapply type_let; [done|apply type_bool_instr|solve_typing|done].
-  Qed.
+  Proof. iIntros. iApply type_let; [apply type_bool_instr|solve_typing|done]. Qed.
 
   Lemma type_if E L C T e1 e2 p:
     (p ◁ bool)%TC ∈ T →
-    typed_body E L C T e1 → typed_body E L C T e2 →
+    typed_body E L C T e1 -∗ typed_body E L C T e2 -∗
     typed_body E L C T (if: p then e1 else e2).
   Proof.
-    iIntros (Hp He1 He2) "!#". iIntros (tid qE) "#LFT Htl HE HL HC HT".
+    iIntros (Hp) "#He1 #He2 !#". iIntros (tid qE) "#LFT Htl HE HL HC HT".
     iDestruct (big_sepL_elem_of _ _ _ Hp with "HT") as "#Hp".
     wp_bind p. iApply (wp_hasty with "Hp").
     iIntros ([[| |[|[]|]]|]) "_ H1"; try done; (iApply wp_case; [done..|iNext]).
-    - iApply (He2 with "LFT Htl HE HL HC HT").
-    - iApply (He1 with "LFT Htl HE HL HC HT").
+    - iApply ("He2" with "LFT Htl HE HL HC HT").
+    - iApply ("He1" with "LFT Htl HE HL HC HT").
   Qed.
 End typing.
diff --git a/theories/typing/borrow.v b/theories/typing/borrow.v
index 23f73999715715ab8ca11594e7c8bf4472199f6d..2ad78a0c229c7f45363498a5456259e5e4c210df 100644
--- a/theories/typing/borrow.v
+++ b/theories/typing/borrow.v
@@ -69,11 +69,9 @@ Section borrow.
     Closed (x :b: []) e →
     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)) →
+    (∀ (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).
-  Proof.
-    intros. eapply type_let; [done|by apply type_deref_uniq_own_instr|solve_typing|done].
-  Qed.
+  Proof. iIntros. iApply type_let; [by apply type_deref_uniq_own_instr|solve_typing|done]. Qed.
 
   Lemma type_deref_shr_own_instr {E L} κ p n ty :
     lctx_lft_alive E L κ →
@@ -97,11 +95,9 @@ Section borrow.
     Closed (x :b: []) e →
     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)) →
+    (∀ (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).
-  Proof.
-    intros. eapply type_let; [done|by apply type_deref_shr_own_instr|solve_typing|done].
-  Qed.
+  Proof. iIntros. iApply type_let; [by apply type_deref_shr_own_instr|solve_typing|done]. Qed.
 
   Lemma type_deref_uniq_uniq_instr {E L} κ κ' p ty :
     lctx_lft_alive E L κ → lctx_lft_incl E L κ κ' →
@@ -133,11 +129,9 @@ Section borrow.
     Closed (x :b: []) e →
     tctx_extract_hasty E L p (&uniq{κ} &uniq{κ'} ty) T T' →
     lctx_lft_alive E L κ → lctx_lft_incl E L κ κ' →
-    (∀ (v:val), typed_body E L C ((v ◁ &uniq{κ} ty) :: T') (subst' x v e)) →
+    (∀ (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).
-  Proof.
-    intros. eapply type_let; [done|by apply type_deref_uniq_uniq_instr|solve_typing|done].
-  Qed.
+  Proof. iIntros. iApply type_let; [by apply type_deref_uniq_uniq_instr|solve_typing|done]. Qed.
 
   Lemma type_deref_shr_uniq_instr {E L} κ κ' p ty :
     lctx_lft_alive E L κ → lctx_lft_incl E L κ κ' →
@@ -167,11 +161,9 @@ Section borrow.
     Closed (x :b: []) e →
     tctx_extract_hasty E L p (&shr{κ} &uniq{κ'} ty) T T' →
     lctx_lft_alive E L κ → lctx_lft_incl E L κ κ' →
-    (∀ (v:val), typed_body E L C ((v ◁ &shr{κ} ty) :: T') (subst' x v e)) →
+    (∀ (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).
-  Proof.
-    intros. eapply type_let; [done|by apply type_deref_shr_uniq_instr|solve_typing|done].
-  Qed.
+  Proof. iIntros. iApply type_let; [by apply type_deref_shr_uniq_instr|solve_typing|done]. Qed.
 End borrow.
 
 Hint Resolve tctx_extract_hasty_borrow tctx_extract_hasty_borrow_share
diff --git a/theories/typing/cont.v b/theories/typing/cont.v
index 48d94ceb8d76bff3a10e56f81b64d0368a7e53c7..7331c523ae463de44a4ed9c84c763adbe3920faa 100644
--- a/theories/typing/cont.v
+++ b/theories/typing/cont.v
@@ -21,20 +21,19 @@ Section typing.
 
   Lemma type_cont argsb L1 (T' : vec val (length argsb) → _) E L2 C T econt e2 kb :
     Closed (kb :b: argsb +b+ []) econt → Closed (kb :b: []) e2 →
-    (∀ k, typed_body E L2 (k ◁cont(L1, T') :: C) T (subst' kb k e2)) →
+    (∀ k, typed_body E L2 (k ◁cont(L1, T') :: C) T (subst' kb k e2)) -∗
     (∀ k (args : vec val (length argsb)),
-       typed_body E L1 (k ◁cont(L1, T') :: C) (T' args) (subst_v (kb::argsb) (k:::args) econt)) →
+       typed_body E L1 (k ◁cont(L1, T') :: C) (T' args) (subst_v (kb::argsb) (k:::args) econt)) -∗
     typed_body E L2 C T (e2 cont: kb argsb := econt).
   Proof.
-    iIntros (Hc1 Hc2 He2 Hecont) "!#". iIntros (tid qE) "#LFT Htl HE HL HC HT". iApply wp_let'.
+    iIntros (Hc1 Hc2) "#He2 #Hecont !#". iIntros (tid qE) "#LFT Htl HE HL HC HT". iApply wp_let'.
     { simpl. rewrite decide_left. done. }
-    iModIntro. iApply (He2 with "LFT Htl HE HL [HC] HT"). clear He2.
+    iModIntro. iApply ("He2" with "LFT Htl HE HL [HC] HT"). iClear "He2".
     iIntros "HE". iLöb as "IH". iIntros (x) "H".
     iDestruct "H" as %[->|?]%elem_of_cons; last by iApply ("HC" with "HE").
     iIntros (args) "Htl HL HT". iApply wp_rec; try done.
     { rewrite Forall_fmap Forall_forall=>? _. rewrite /= to_of_val. eauto. }
     { by rewrite -(subst_v_eq (_ :: _) (RecV _ _ _ ::: _)). }
-    iNext. iApply (Hecont with "LFT Htl HE HL [HC] HT").
-    by iApply "IH".
+    iNext. iApply ("Hecont" with "LFT Htl HE HL [HC] HT"). by iApply "IH".
   Qed.
 End typing.
diff --git a/theories/typing/examples/get_x.v b/theories/typing/examples/get_x.v
index 7b9dc2dd6f629132b439ee78a8efd85567f82bcc..186d39a5f54a1d2433c49365e23fdfee63a700a3 100644
--- a/theories/typing/examples/get_x.v
+++ b/theories/typing/examples/get_x.v
@@ -1,3 +1,4 @@
+From iris.proofmode Require Export tactics.
 From lrust.typing Require Import typing.
 Set Default Proof Using "Type".
 
@@ -17,11 +18,12 @@ Section get_x.
      and without using 'typed_instruction_ty'.  I think that's related to
      the list notation that we added to %TC. *)
   Proof.
-    eapply type_fn; [solve_typing..|]=> /= α ret p. inv_vec p=>p. simpl_subst.
-    eapply type_deref; [solve_typing..|by apply read_own_move|done|].
-      intros p'; simpl_subst.
-    eapply (type_letalloc_1 (&shr{α}int)); [solve_typing..|]=>r. simpl_subst.
-    eapply type_delete; [solve_typing..|].
-    eapply (type_jump [_]); solve_typing.
+    iApply type_fn; [solve_typing..|]. simpl. iIntros (α ret p).
+    inv_vec p=>p. simpl_subst.
+    iApply type_deref; [solve_typing..|by apply read_own_move|done|].
+      iIntros (p'); simpl_subst.
+    iApply (type_letalloc_1 (&shr{α}int)); [solve_typing..|]. iIntros (r). simpl_subst.
+    iApply type_delete; [solve_typing..|].
+    iApply (type_jump [_]); solve_typing.
   Qed.
 End get_x.
diff --git a/theories/typing/examples/init_prod.v b/theories/typing/examples/init_prod.v
index 967f4735fed4a8198695c9ef4cd0c0b44caefa61..44c0c100647d9c88b9b369645b1544d22d626ca2 100644
--- a/theories/typing/examples/init_prod.v
+++ b/theories/typing/examples/init_prod.v
@@ -1,3 +1,4 @@
+From iris.proofmode Require Export tactics.
 From lrust.typing Require Import typing.
 Set Default Proof Using "Type".
 
@@ -15,15 +16,15 @@ Section init_prod.
     typed_instruction_ty [] [] [] init_prod
         (fn([]; int, int) → Π[int;int]).
   Proof.
-    eapply type_fn; [solve_typing..|]=>- /= [] ret p. inv_vec p=>x y. simpl_subst.
-    eapply type_deref; [solve_typing..|apply read_own_move|done|]=>x'. simpl_subst.
-    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_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..|].
-    eapply (type_jump [_]); solve_typing.
+    iApply type_fn; [solve_typing..|]. simpl. iIntros ([] ret p). inv_vec p=>x y. simpl_subst.
+    iApply type_deref; [solve_typing..|apply read_own_move|done|]. iIntros (x'). simpl_subst.
+    iApply type_deref; [solve_typing..|apply read_own_move|done|]. iIntros (y'). simpl_subst.
+    iApply (type_new_subtype (Π[uninit 1; uninit 1])); [solve_typing..|].
+      iIntros (r). simpl_subst. unfold Z.to_nat, Pos.to_nat; simpl.
+    iApply (type_assign (own_ptr 2 (uninit 1))); [solve_typing..|by apply write_own|].
+    iApply type_assign; [solve_typing..|by apply write_own|].
+    iApply type_delete; [solve_typing..|].
+    iApply type_delete; [solve_typing..|].
+    iApply (type_jump [_]); solve_typing.
   Qed.
 End init_prod.
diff --git a/theories/typing/examples/lazy_lft.v b/theories/typing/examples/lazy_lft.v
index e7f2c877ab15db7913a315c16f5ab6014edb0606..58acc6f5a75bd3540d493d1a10ec2bff656e9794 100644
--- a/theories/typing/examples/lazy_lft.v
+++ b/theories/typing/examples/lazy_lft.v
@@ -1,3 +1,4 @@
+From iris.proofmode Require Export tactics.
 From lrust.typing Require Import typing.
 Set Default Proof Using "Type".
 
@@ -20,26 +21,26 @@ Section lazy_lft.
     typed_instruction_ty [] [] [] lazy_lft
         (fn([]) → unit).
   Proof.
-    eapply type_fn; [solve_typing..|]=>- /= [] ret p. inv_vec p. simpl_subst.
-    eapply (type_newlft []); [solve_typing|]=>α.
-    eapply (type_new_subtype (Π[uninit 1;uninit 1])); [solve_typing..|].
-      intros t. simpl_subst.
-    eapply type_new; [solve_typing..|]=>f. simpl_subst.
-    eapply type_new; [solve_typing..|]=>g. simpl_subst.
-    eapply type_int; [solve_typing|]=>v42. simpl_subst.
-    eapply type_assign; [solve_typing..|by eapply write_own|].
-    eapply (type_assign _ (&shr{α}_)); [solve_typing..|by eapply write_own|].
-    eapply type_assign; [solve_typing..|by eapply write_own|].
-    eapply type_deref; [solve_typing..|apply: read_own_copy|done|]=>t0'. simpl_subst.
-    eapply type_letpath; [solve_typing..|]=>dummy. simpl_subst.
-    eapply type_int; [solve_typing|]=>v23. simpl_subst.
-    eapply type_assign; [solve_typing..|by eapply write_own|].
-    eapply (type_assign _ (&shr{α}int)); [solve_typing..|by eapply write_own|].
-    eapply type_new; [solve_typing..|] =>r. simpl_subst.
-    eapply type_endlft; [solve_typing..|].
-    eapply (type_delete (Π[&shr{_}_;&shr{_}_])%T); [solve_typing..|].
-    eapply type_delete; [solve_typing..|].
-    eapply type_delete; [solve_typing..|].
-    eapply (type_jump [_]); solve_typing.
+    iApply type_fn; [solve_typing..|]. simpl. iIntros ([] ret p). inv_vec p. simpl_subst.
+    iApply (type_newlft []). iIntros (α).
+    iApply (type_new_subtype (Π[uninit 1;uninit 1])); [solve_typing..|].
+      iIntros (t). simpl_subst.
+    iApply type_new; [solve_typing|]. iIntros (f). simpl_subst.
+    iApply type_new; [solve_typing|]. iIntros (g). simpl_subst.
+    iApply type_int. iIntros (v42). simpl_subst.
+    iApply type_assign; [solve_typing|by eapply write_own|].
+    iApply (type_assign _ (&shr{α}_)); [solve_typing..|by eapply write_own|].
+    iApply type_assign; [solve_typing|by eapply write_own|].
+    iApply type_deref; [solve_typing|apply: read_own_copy|done|]. iIntros (t0'). simpl_subst.
+    iApply type_letpath; [solve_typing|]. iIntros (dummy). simpl_subst.
+    iApply type_int. iIntros (v23). simpl_subst.
+    iApply type_assign; [solve_typing|by eapply write_own|].
+    iApply (type_assign _ (&shr{α}int)); [solve_typing..|by eapply write_own|].
+    iApply type_new; [solve_typing..|]. iIntros (r). simpl_subst.
+    iApply type_endlft; [solve_typing..|].
+    iApply (type_delete (Π[&shr{_}_;&shr{_}_])%T); [solve_typing..|].
+    iApply type_delete; [solve_typing..|].
+    iApply type_delete; [solve_typing..|].
+    iApply (type_jump [_]); solve_typing.
   Qed.
 End lazy_lft.
diff --git a/theories/typing/examples/option_as_mut.v b/theories/typing/examples/option_as_mut.v
index 2ede44183b1b3326eed185f262d52bd4d6c87d7b..8a004b017a48b6f21652df440b02eb42adcf2aff 100644
--- a/theories/typing/examples/option_as_mut.v
+++ b/theories/typing/examples/option_as_mut.v
@@ -1,3 +1,4 @@
+From iris.proofmode Require Export tactics.
 From lrust.typing Require Import typing.
 Set Default Proof Using "Type".
 
@@ -18,19 +19,19 @@ Section option_as_mut.
     typed_instruction_ty [] [] [] option_as_mut
         (fn(∀ α, [☀α]; &uniq{α} Σ[unit; τ]) → Σ[unit; &uniq{α}τ]).
   Proof.
-    eapply type_fn; [solve_typing..|]=> /= α ret p. inv_vec p=>o. simpl_subst.
-    eapply (type_cont [_] [] (λ r, [o ◁ _; r!!!0 ◁ _])%TC) ; [solve_typing..| |].
-    - intros k. simpl_subst.
-      eapply type_deref; [solve_typing..|apply read_own_move|done|]=>o'. simpl_subst.
-      eapply type_new; [solve_typing..|]. intros r. simpl_subst.
-      eapply type_case_uniq; [solve_typing..|].
+    iApply type_fn; [solve_typing..|]. simpl. iIntros (α ret p). inv_vec p=>o. simpl_subst.
+    iApply (type_cont [_] [] (λ r, [o ◁ _; r!!!0 ◁ _])%TC) ; [solve_typing..| |].
+    - iIntros (k). simpl_subst.
+      iApply type_deref; [solve_typing|apply read_own_move|done|]. iIntros (o'). simpl_subst.
+      iApply type_new; [solve_typing..|]. iIntros (r). simpl_subst.
+      iApply type_case_uniq; [solve_typing..|].
         constructor; last constructor; last constructor; left.
-      + eapply (type_sum_assign_unit [unit; &uniq{α}τ]%T); [solve_typing..|by apply write_own|].
-        eapply (type_jump [_]); solve_typing.
-      + eapply (type_sum_assign [unit; &uniq{α}τ]%T); [solve_typing..|by apply write_own|].
-        eapply (type_jump [_]); solve_typing.
-    - move=>/= k r. inv_vec r=>r. simpl_subst.
-      eapply type_delete; [solve_typing..|].
-      eapply (type_jump [_]); solve_typing.
+      + iApply (type_sum_assign_unit [unit; &uniq{α}τ]%T); [solve_typing..|by apply write_own|].
+        iApply (type_jump [_]); solve_typing.
+      + iApply (type_sum_assign [unit; &uniq{α}τ]%T); [solve_typing..|by apply write_own|].
+        iApply (type_jump [_]); solve_typing.
+    - simpl. iIntros (k r). inv_vec r=>r. simpl_subst.
+      iApply type_delete; [solve_typing..|].
+      iApply (type_jump [_]); solve_typing.
   Qed.
 End option_as_mut.
diff --git a/theories/typing/examples/rebor.v b/theories/typing/examples/rebor.v
index d0403aab7967084998763538f528f28cde1bec6d..1a4103b623a3dd0229410f60d6c2c7c16ebd4e3b 100644
--- a/theories/typing/examples/rebor.v
+++ b/theories/typing/examples/rebor.v
@@ -1,3 +1,4 @@
+From iris.proofmode Require Export tactics.
 From lrust.typing Require Import typing.
 Set Default Proof Using "Type".
 
@@ -19,18 +20,18 @@ Section rebor.
     typed_instruction_ty [] [] [] rebor
         (fn([]; Π[int; int], Π[int; int]) → int).
   Proof.
-    eapply type_fn; [solve_typing..|]=>- /= [] ret p. inv_vec p=>t1 t2. simpl_subst.
-    eapply (type_newlft []). apply _. move=> α.
-    eapply (type_letalloc_1 (&uniq{α}Π[int; int])); [solve_typing..|]=>x. simpl_subst.
-    eapply type_deref; [solve_typing..|apply read_own_move|done|]=>x'. simpl_subst.
-    eapply (type_letpath (&uniq{α}int)); [solve_typing..|]=>y. simpl_subst.
-    eapply (type_assign _ (&uniq{α}Π [int; int])); [solve_typing..|by apply write_own|].
-    eapply type_deref; [solve_typing..|apply: read_uniq; solve_typing|done|]=>y'. simpl_subst.
-    eapply type_letalloc_1; [solve_typing..|]=>r. simpl_subst.
-    eapply type_endlft; [solve_typing..|].
-    eapply type_delete; [solve_typing..|].
-    eapply type_delete; [solve_typing..|].
-    eapply type_delete; [solve_typing..|].
-    eapply (type_jump [_]); solve_typing.
+    iApply type_fn; [solve_typing..|]. simpl. iIntros ([] ret p). inv_vec p=>t1 t2. simpl_subst.
+    iApply (type_newlft []). iIntros (α).
+    iApply (type_letalloc_1 (&uniq{α}Π[int; int])); [solve_typing..|]. iIntros (x). simpl_subst.
+    iApply type_deref; [solve_typing|apply read_own_move|done|]. iIntros (x'). simpl_subst.
+    iApply (type_letpath (&uniq{α}int)); [solve_typing|]. iIntros (y). simpl_subst.
+    iApply (type_assign _ (&uniq{α}Π [int; int])); [solve_typing|by apply write_own|].
+    iApply type_deref; [solve_typing|apply: read_uniq; solve_typing|done|]. iIntros (y'). simpl_subst.
+    iApply type_letalloc_1; [solve_typing..|]. iIntros (r). simpl_subst.
+    iApply type_endlft.
+    iApply type_delete; [solve_typing..|].
+    iApply type_delete; [solve_typing..|].
+    iApply type_delete; [solve_typing..|].
+    iApply (type_jump [_]); solve_typing.
   Qed.
 End rebor.
diff --git a/theories/typing/examples/unbox.v b/theories/typing/examples/unbox.v
index d682ed72cb7ceefe2da0dc9fff5a5433dd9dea79..cabf10707f499f6da26bb50a2507847b5022546e 100644
--- a/theories/typing/examples/unbox.v
+++ b/theories/typing/examples/unbox.v
@@ -1,3 +1,4 @@
+From iris.proofmode Require Export tactics.
 From lrust.typing Require Import typing.
 Set Default Proof Using "Type".
 
@@ -14,12 +15,12 @@ Section unbox.
     typed_instruction_ty [] [] [] unbox
         (fn(∀ α, [☀α]; &uniq{α}box (Π[int; int])) → &uniq{α} int).
   Proof.
-    eapply type_fn; [solve_typing..|]=> /= α ret b. inv_vec b=>b. simpl_subst.
-    eapply type_deref; [solve_typing..|by apply read_own_move|done|].
-    intros b'; simpl_subst.
-    eapply type_deref_uniq_own; [solve_typing..|]=>bx; simpl_subst.
-    eapply type_letalloc_1; [solve_typing..|]=>r. simpl_subst.
-    eapply type_delete; [solve_typing..|].
-    eapply (type_jump [_]); solve_typing.
+    iApply type_fn; [solve_typing..|]. simpl. iIntros (α ret b). inv_vec b=>b. simpl_subst.
+    iApply type_deref; [solve_typing..|by apply read_own_move|done|].
+    iIntros (b'); simpl_subst.
+    iApply type_deref_uniq_own; [solve_typing..|]. iIntros (bx); simpl_subst.
+    iApply type_letalloc_1; [solve_typing..|]. iIntros (r). simpl_subst.
+    iApply type_delete; [solve_typing..|].
+    iApply (type_jump [_]); solve_typing.
   Qed.
 End unbox.
diff --git a/theories/typing/examples/unwrap_or.v b/theories/typing/examples/unwrap_or.v
index dcc0cb8b1f6ca7b04c5876806c75c60cfca817e3..e4584e02fd354cfa92c3c115b5ffccd1dca4611c 100644
--- a/theories/typing/examples/unwrap_or.v
+++ b/theories/typing/examples/unwrap_or.v
@@ -1,3 +1,4 @@
+From iris.proofmode Require Export tactics.
 From lrust.typing Require Import typing.
 Set Default Proof Using "Type".
 
@@ -15,14 +16,14 @@ Section unwrap_or.
     typed_instruction_ty [] [] [] (unwrap_or Ï„)
         (fn([]; Σ[unit; τ], τ) → τ).
   Proof.
-    eapply type_fn; [solve_typing..|]=>- /= [] ret p. inv_vec p=>o def. simpl_subst.
-    eapply type_case_own; [solve_typing..|]. constructor; last constructor; last constructor.
-    + right. eapply type_delete; [solve_typing..|].
-      eapply (type_jump [_]); solve_typing.
-    + left. eapply type_letalloc_n; [solve_typing..|by apply read_own_move|]=>r.
+    iApply type_fn; [solve_typing..|]. simpl. iIntros ([] ret p). inv_vec p=>o def. simpl_subst.
+    iApply type_case_own; [solve_typing|]. constructor; last constructor; last constructor.
+    + right. iApply type_delete; [solve_typing..|].
+      iApply (type_jump [_]); solve_typing.
+    + left. iApply type_letalloc_n; [solve_typing|by apply read_own_move|]. iIntros (r).
         simpl_subst.
-      eapply (type_delete (Π[uninit _;uninit _;uninit _])); [solve_typing..|].
-      eapply type_delete; [solve_typing..|].
-      eapply (type_jump [_]); solve_typing.
+      iApply (type_delete (Π[uninit _;uninit _;uninit _])); [solve_typing..|].
+      iApply type_delete; [solve_typing..|].
+      iApply (type_jump [_]); solve_typing.
   Qed.
 End unwrap_or.
diff --git a/theories/typing/function.v b/theories/typing/function.v
index 6cecb4cf2c49dac7345475680368101e3beb36cf..5c67b11688a6fd9a68b6c39ec0fceb4dfbcf7055 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -250,10 +250,10 @@ Section typing.
     elctx_sat E L (E' x) →
     tctx_extract_ctx E L (zip_with TCtx_hasty ps
                                    ((λ ty, box ty) <$> vec_to_list (tys x))) T T' →
-    (∀ ret : val, typed_body E L C ((ret ◁ box (ty x))::T') (subst' b ret e)) →
+    (∀ ret : val, typed_body E L C ((ret ◁ box (ty x))::T') (subst' b ret e)) -∗
     typed_body E L C T (letcall: b := p ps in e).
   Proof.
-    intros ?? Hpsc ????. eapply (type_cont [_] _ (λ r, (r!!!0 ◁ box (ty x)) :: T')%TC).
+    iIntros (?? Hpsc ???) "He". iApply (type_cont [_] _ (λ r, (r!!!0 ◁ box (ty x)) :: T')%TC).
     - (* TODO : make [solve_closed] work here. *)
       eapply is_closed_weaken; first done. set_solver+.
     - (* TODO : make [solve_closed] work here. *)
@@ -261,17 +261,19 @@ Section typing.
       + by eapply is_closed_weaken, list_subseteq_nil.
       + eapply Is_true_eq_left, forallb_forall, List.Forall_forall, Forall_impl=>//.
         intros. eapply Is_true_eq_true, is_closed_weaken=>//. set_solver+.
-    - intros.
+    - iIntros (k).
       (* TODO : make [simpl_subst] work here. *)
       change (subst' "_k" k (p (Var "_k" :: ps))) with
              ((subst "_k" k p) (of_val k :: map (subst "_k" k) ps)).
       rewrite is_closed_nil_subst //.
       assert (map (subst "_k" k) ps = ps) as ->.
       { clear -Hpsc. induction Hpsc=>//=. rewrite is_closed_nil_subst //. congruence. }
-      eapply type_call; try done. constructor. done.
-    - move=>/= k ret. inv_vec ret=>ret. rewrite /subst_v /=.
-      rewrite ->(is_closed_subst []), incl_cctx_incl; first done; try set_solver+.
-      apply subst'_is_closed; last done. apply is_closed_of_val.
+      iApply type_call; try done. constructor. done.
+    - simpl. iIntros (k ret). inv_vec ret=>ret. rewrite /subst_v /=.
+      rewrite ->(is_closed_subst []); last set_solver+; last first.
+      { apply subst'_is_closed; last done. apply is_closed_of_val. }
+      (iApply typed_body_mono; last by iApply "He"); [|done..].
+      apply incl_cctx_incl. set_solver+.
   Qed.
 
   Lemma type_rec {A} E L E' fb (argsb : list binder) ef e n
@@ -285,16 +287,16 @@ Section typing.
                    ((f ◁ fn E' tys ty) ::
                       zip_with (TCtx_hasty ∘ of_val) args
                                ((λ ty, box ty) <$> vec_to_list (tys x)) ++ T)
-                   (subst_v (fb :: BNamed "return" :: argsb) (f ::: k ::: args) e)) →
+                   (subst_v (fb :: BNamed "return" :: argsb) (f ::: k ::: args) e)) -∗
     typed_instruction_ty E L T ef (fn E' tys ty).
   Proof.
-    iIntros (-> -> Hc Hbody) "!# * #LFT $ $ $ #HT". iApply wp_value.
+    iIntros (-> -> Hc) "#Hbody !# * #LFT $ $ $ #HT". iApply wp_value.
     { simpl. rewrite ->(decide_left Hc). done. }
     rewrite tctx_interp_singleton. iLöb as "IH". iExists _. iSplit.
     { simpl. rewrite decide_left. done. }
     iExists fb, _, argsb, e, _. iSplit. done. iSplit. done. iNext. clear qE.
     iIntros (x k args) "!#". iIntros (tid' qE) "_ Htl HE HL HC HT'".
-    iApply (Hbody with "LFT Htl HE HL HC").
+    iApply ("Hbody" with "LFT Htl HE HL HC").
     rewrite tctx_interp_cons tctx_interp_app. iFrame "HT' IH".
     by iApply sendc_change_tid.
   Qed.
@@ -309,10 +311,11 @@ Section typing.
         typed_body (E' x) [] [k ◁cont([], λ v : vec _ 1, [v!!!0 ◁ box (ty x)])]
                    (zip_with (TCtx_hasty ∘ of_val) args
                              ((λ ty, box ty) <$> vec_to_list (tys x)) ++ T)
-                   (subst_v (BNamed "return" :: argsb) (k ::: args) e)) →
+                   (subst_v (BNamed "return" :: argsb) (k ::: args) e)) -∗
     typed_instruction_ty E L T ef (fn E' tys ty).
   Proof.
-    intros. eapply type_rec; try done. intros. rewrite -typed_body_mono //=.
+    iIntros (???) "He". iApply type_rec; try done. iIntros.
+    (iApply typed_body_mono; last by iApply "He"); try done.
     eapply contains_tctx_incl. by constructor.
   Qed.
 End typing.
diff --git a/theories/typing/int.v b/theories/typing/int.v
index d4d04fd1dc18d52686cadfac727c84619705d0c9..2dd8f6923631e9bafe05cb125463b7cf1273a23c 100644
--- a/theories/typing/int.v
+++ b/theories/typing/int.v
@@ -31,11 +31,9 @@ Section typing.
 
   Lemma type_int (z : Z) E L C T x e :
     Closed (x :b: []) e →
-    (∀ (v : val), typed_body E L C ((v ◁ int) :: T) (subst' x v e)) →
+    (∀ (v : val), typed_body E L C ((v ◁ int) :: T) (subst' x v e)) -∗
     typed_body E L C T (let: x := #z in e).
-  Proof.
-    intros. eapply type_let; [done|apply type_int_instr|solve_typing|done].
-  Qed.
+  Proof. iIntros. iApply type_let; [apply type_int_instr|solve_typing|done]. Qed.
 
   Lemma type_plus_instr E L p1 p2 :
     typed_instruction_ty E L [p1 ◁ int; p2 ◁ int] (p1 + p2) int.
@@ -50,11 +48,9 @@ Section typing.
   Lemma type_plus E L C T T' p1 p2 x e :
     Closed (x :b: []) e →
     tctx_extract_ctx E L [p1 ◁ int; p2 ◁ int] T T' →
-    (∀ (v : val), typed_body E L C ((v ◁ int) :: T') (subst' x v e)) →
+    (∀ (v : val), typed_body E L C ((v ◁ int) :: T') (subst' x v e)) -∗
     typed_body E L C T (let: x := p1 + p2 in e).
-  Proof.
-    intros. eapply type_let; [done|apply type_plus_instr|solve_typing|done].
-  Qed.
+  Proof. iIntros. iApply type_let; [iApply type_plus_instr|solve_typing|done]. Qed.
 
   Lemma type_minus_instr E L p1 p2 :
     typed_instruction_ty E L [p1 ◁ int; p2 ◁ int] (p1 - p2) int.
@@ -69,11 +65,9 @@ Section typing.
   Lemma type_minus E L C T T' p1 p2 x e :
     Closed (x :b: []) e →
     tctx_extract_ctx E L [p1 ◁ int; p2 ◁ int] T T' →
-    (∀ (v : val), typed_body E L C ((v ◁ int) :: T') (subst' x v e)) →
+    (∀ (v : val), typed_body E L C ((v ◁ int) :: T') (subst' x v e)) -∗
     typed_body E L C T (let: x := p1 - p2 in e).
-  Proof.
-    intros. eapply type_let; [done|apply type_minus_instr|solve_typing|done].
-  Qed.
+  Proof. iIntros. iApply type_let; [apply type_minus_instr|solve_typing|done]. Qed.
 
   Lemma type_le_instr E L p1 p2 :
     typed_instruction_ty E L [p1 ◁ int; p2 ◁ int] (p1 ≤ p2) bool.
@@ -88,9 +82,7 @@ Section typing.
   Lemma type_le E L C T T' p1 p2 x e :
     Closed (x :b: []) e →
     tctx_extract_ctx E L [p1 ◁ int; p2 ◁ int] T T' →
-    (∀ (v : val), typed_body E L C ((v ◁ bool) :: T') (subst' x v e)) →
+    (∀ (v : val), typed_body E L C ((v ◁ bool) :: T') (subst' x v e)) -∗
     typed_body E L C T (let: x := p1 ≤ p2 in e).
-  Proof.
-    intros. eapply type_let; [done|apply type_le_instr|solve_typing|done].
-  Qed.
+  Proof. iIntros. iApply type_let; [apply type_le_instr|solve_typing|done]. Qed.
 End typing.
diff --git a/theories/typing/own.v b/theories/typing/own.v
index 0bb33dda2d6ecdbe40b462bb9b583d071c94534f..d86aca228e05073849f1159632584a21b0fedd23 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -206,20 +206,20 @@ Section typing.
     Closed (x :b: []) e →
     0 ≤ n →
     (∀ (v : val) (n' := Z.to_nat n),
-        typed_body E L C ((v ◁ box (uninit n')) :: T) (subst' x v e)) →
+        typed_body E L C ((v ◁ box (uninit n')) :: T) (subst' x v e)) -∗
     typed_body E L C T (let: x := new [ #n ] in e).
-  Proof. intros. eapply type_let; [done|by apply type_new_instr|solve_typing..]. Qed.
+  Proof. iIntros. iApply type_let; [by apply type_new_instr|solve_typing..]. Qed.
 
   Lemma type_new_subtype ty E L C T x (n : Z) e :
     Closed (x :b: []) e →
     0 ≤ n →
     let n' := Z.to_nat n in
     subtype E L (uninit n') ty →
-    (∀ (v : val), typed_body E L C ((v ◁ own_ptr 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.
-    iIntros (v). iApply typed_body_mono; [done| |done|by iApply (Htyp v)].
+    iIntros (????) "Htyp". iApply type_let; [by apply type_new_instr|solve_typing|].
+    iIntros (v). iApply typed_body_mono; last iApply "Htyp"; try done.
     by apply (tctx_incl_frame_r _ [_] [_]), subtype_tctx_incl, own_mono.
   Qed.
 
@@ -239,10 +239,10 @@ Section typing.
     Closed [] e →
     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' e -∗
     typed_body E L C T (delete [ #n; p ] ;; e).
   Proof.
-    intros ?? -> Hlen ?. eapply type_seq; [done|by apply type_delete_instr| |done].
+    iIntros (?? -> Hlen) "?". iApply type_seq; [by apply type_delete_instr| |done].
     by rewrite (inj _ _ _ Hlen).
   Qed.
 
@@ -250,20 +250,20 @@ 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_ptr 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.
+    iIntros. iApply type_new.
     - rewrite /Closed /=. rewrite !andb_True.
       eauto 10 using is_closed_weaken with set_solver.
     - done.
-    - move=>xv /=.
+    - iIntros (xv) "/=".
       assert (subst x xv (x <- p ;; e)%E = (xv <- p ;; subst x xv e)%E) as ->.
       { (* TODO : simpl_subst should be able to do this. *)
         unfold subst=>/=. repeat f_equal.
         - by rewrite bool_decide_true.
         - eapply is_closed_subst. done. set_solver. }
-      eapply type_assign; [|solve_typing|by eapply write_own|done].
+      iApply type_assign; [|solve_typing|by eapply write_own|done].
       apply subst_is_closed; last done. apply is_closed_of_val.
   Qed.
 
@@ -272,14 +272,14 @@ Section typing.
     tctx_extract_hasty E L p ty1 T T' →
     typed_read E L ty1 ty ty2 →
     (∀ (v : val),
-        typed_body E L C ((v ◁ own_ptr (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.
+    iIntros. iApply type_new.
     - rewrite /Closed /=. rewrite !andb_True.
       eauto 10 using is_closed_of_val, is_closed_weaken with set_solver.
     - lia.
-    - move=>xv /=.
+    - iIntros (xv) "/=".
       assert (subst x xv (x <-{ty.(ty_size)} !p ;; e)%E =
               (xv <-{ty.(ty_size)} !p ;; subst x xv e)%E) as ->.
       { (* TODO : simpl_subst should be able to do this. *)
@@ -287,7 +287,7 @@ Section typing.
         - eapply (is_closed_subst []). apply is_closed_of_val. set_solver.
         - by rewrite bool_decide_true.
         - eapply is_closed_subst. done. set_solver. }
-      rewrite Nat2Z.id. eapply type_memcpy.
+      rewrite Nat2Z.id. iApply type_memcpy.
       + apply subst_is_closed; last done. apply is_closed_of_val.
       + solve_typing.
       + (* TODO: Doing "eassumption" here shows that unification takes *forever* to fail.
diff --git a/theories/typing/programs.v b/theories/typing/programs.v
index 7a480ffc60450dfcbf030031f0a490de82a6e684..544e960f157f2fe0299845c9790c70536fef37f9 100644
--- a/theories/typing/programs.v
+++ b/theories/typing/programs.v
@@ -88,7 +88,7 @@ Section typing_rules.
   (* This lemma is helpful when switching from proving unsafe code in Iris
      back to proving it in the type system. *)
   Lemma type_type E L C T e :
-    typed_body E L C T e → typed_body E L C T e.
+    typed_body E L C T e -∗ typed_body E L C T e.
   Proof. done. Qed.
 
   (* TODO: notation scopes need tuing to avoid the %list here. *)
@@ -109,43 +109,51 @@ Section typing_rules.
 
   Lemma type_let' E L T1 T2 (T : tctx) C xb e e' :
     Closed (xb :b: []) e' →
-    typed_instruction E L T1 e T2 →
-    (∀ v : val, typed_body E L C (T2 v ++ T) (subst' xb v e')) →
+    typed_instruction E L T1 e T2 -∗
+    (∀ v : val, typed_body E L C (T2 v ++ T) (subst' xb v e')) -∗
     typed_body E L C (T1 ++ T) (let: xb := e in e').
   Proof.
-    iIntros (Hc He He') "!#". iIntros (tid qE) "#LFT Htl HE HL HC HT". rewrite tctx_interp_app.
+    iIntros (Hc) "#He #He' !#". iIntros (tid qE) "#LFT Htl HE HL HC HT". rewrite tctx_interp_app.
     iDestruct "HT" as "[HT1 HT]". wp_bind e. iApply (wp_wand with "[HE HL HT1 Htl]").
-    { iApply (He with "LFT Htl HE HL HT1"). }
+    { iApply ("He" with "LFT Htl HE HL HT1"). }
     iIntros (v) "/= (Htl & HE & HL & HT2)". iApply wp_let; first wp_done.
-    iModIntro. iApply (He' with "LFT Htl HE HL HC [HT2 HT]").
+    iModIntro. iApply ("He'" with "LFT Htl HE HL HC [HT2 HT]").
     rewrite tctx_interp_app. by iFrame.
   Qed.
 
+  (* We do not make the [typed_instruction] hypothesis part of the
+     Iris hypotheses, because we want to preserve the order of the
+     hypotheses. The is important, since proving [typed_instruction]
+     will instantiate [T1] and [T2], and hence we know what to search
+     for the following hypothesis. *)
   Lemma type_let E L T T' T1 T2 C xb e e' :
     Closed (xb :b: []) e' →
     typed_instruction E L T1 e T2 →
     tctx_extract_ctx E L T1 T T' →
-    (∀ v : val, typed_body E L C (T2 v ++ T') (subst' xb v e')) →
+    (∀ v : val, typed_body E L C (T2 v ++ T') (subst' xb v e')) -∗
     typed_body E L C T (let: xb := e in e').
-  Proof. unfold tctx_extract_ctx. intros ?? -> ?. by eapply type_let'. Qed.
+  Proof.
+    unfold tctx_extract_ctx. iIntros (? He ->) "?". iApply type_let'; last done.
+    iApply He.
+  Qed.
 
   Lemma type_seq E L T T' T1 T2 C e e' :
     Closed [] e' →
     typed_instruction E L T1 e (λ _, T2) →
     tctx_extract_ctx E L T1 T T' →
-    (typed_body E L C (T2 ++ T') e') →
+    typed_body E L C (T2 ++ T') e' -∗
     typed_body E L C T (e ;; e').
-  Proof. intros. by eapply (type_let E L T T' T1 (λ _, T2)). Qed.
+  Proof. iIntros. iApply (type_let E L T T' T1 (λ _, T2)); auto. Qed.
 
   Lemma type_newlft {E L C T} κs e :
     Closed [] e →
-    (∀ κ, typed_body E ((κ ⊑ κs) :: L) C T e) →
+    (∀ κ, typed_body E ((κ ⊑ κs) :: L) C T e) -∗
     typed_body E L C T (Newlft ;; e).
   Proof.
-    iIntros (Hc He) "!#". iIntros (tid qE) "#LFT Htl HE HL HC HT".
+    iIntros (Hc) "#He !#". iIntros (tid qE) "#LFT Htl HE HL HC HT".
     iMod (lft_create with "LFT") as (Λ) "[Htk #Hinh]"; first done.
     set (κ' := foldr (∪) static κs). wp_seq.
-    iApply (He (κ' ∪ Λ) with "LFT Htl HE [HL Htk] HC HT").
+    iApply ("He" $! (κ' ∪ Λ) with "LFT Htl HE [HL Htk] HC HT").
     rewrite /llctx_interp big_sepL_cons. iFrame "HL".
     iExists Λ. iSplit; first done. iFrame. done.
   Qed.
@@ -154,13 +162,14 @@ Section typing_rules.
      Right now, we could take two. *)
   Lemma type_endlft E L C T1 T2 κ κs e :
     Closed [] e → UnblockTctx κ T1 T2 →
-    typed_body E L C T2 e → typed_body E ((κ ⊑ κs) :: L) C T1 (Endlft ;; e).
+    typed_body E L C T2 e -∗ typed_body E ((κ ⊑ κs) :: L) C T1 (Endlft ;; e).
   Proof.
-    iIntros (Hc Hub He) "!#". iIntros (tid qE) "#LFT Htl HE". rewrite /llctx_interp big_sepL_cons.
-    iIntros "[Hκ HL] HC HT". iDestruct "Hκ" as (Λ) "(% & Htok & #Hend)".
+    iIntros (Hc Hub) "#He !#". iIntros (tid qE) "#LFT Htl HE".
+    rewrite /llctx_interp big_sepL_cons. iIntros "[Hκ HL] HC HT".
+    iDestruct "Hκ" as (Λ) "(% & Htok & #Hend)".
     iSpecialize ("Hend" with "Htok"). wp_bind Endlft.
     iApply (wp_fupd_step with "Hend"); try done. wp_seq.
-    iIntros "#Hdead !>". wp_seq. iApply (He with "LFT Htl HE HL HC >").
+    iIntros "#Hdead !>". wp_seq. iApply ("He" with "LFT Htl HE HL HC >").
     iApply (Hub with "[] HT"). simpl in *. subst κ. rewrite -lft_dead_or. auto.
   Qed.
 
@@ -175,11 +184,9 @@ Section typing_rules.
   Lemma type_letpath {E L} ty C T T' x p e :
     Closed (x :b: []) e →
     tctx_extract_hasty E L p ty T T' →
-    (∀ (v : val), typed_body E L C ((v ◁ ty) :: T') (subst' x v e)) →
+    (∀ (v : val), typed_body E L C ((v ◁ ty) :: T') (subst' x v e)) -∗
     typed_body E L C T (let: x := p in e).
-  Proof.
-    intros. eapply type_let; [done|by apply type_path_instr|solve_typing|by simpl].
-  Qed.
+  Proof. iIntros. iApply type_let; [by apply type_path_instr|solve_typing|done]. Qed.
 
   Lemma type_assign_instr {E L} ty ty1 ty1' p1 p2 :
     typed_write E L ty1 ty ty1' →
@@ -203,9 +210,9 @@ Section typing_rules.
     Closed [] e →
     tctx_extract_ctx E L [p1 ◁ ty1; p2 ◁ ty] T T' →
     typed_write E L ty1 ty ty1' →
-    typed_body E L C ((p1 ◁ ty1') :: T') e →
+    typed_body E L C ((p1 ◁ ty1') :: T') e -∗
     typed_body E L C T (p1 <- p2 ;; e).
-  Proof. intros. eapply type_seq; [done |by apply type_assign_instr|done|done]. Qed.
+  Proof. iIntros. by iApply type_seq; first apply type_assign_instr. Qed.
 
   Lemma type_deref_instr {E L} ty ty1 ty1' p :
     ty.(ty_size) = 1%nat → typed_read E L ty1 ty ty1' →
@@ -229,11 +236,9 @@ Section typing_rules.
     tctx_extract_hasty E L p ty1 T T' →
     typed_read E L ty1 ty ty1' →
     ty.(ty_size) = 1%nat →
-    (∀ (v : val), typed_body E L C ((p ◁ ty1') :: (v ◁ ty) :: T') (subst' x v e)) →
+    (∀ (v : val), typed_body E L C ((p ◁ ty1') :: (v ◁ ty) :: T') (subst' x v e)) -∗
     typed_body E L C T (let: x := !p in e).
-  Proof.
-    intros. eapply type_let; [done|by apply type_deref_instr|solve_typing|by simpl].
-  Qed.
+  Proof. iIntros. by iApply type_let; [apply type_deref_instr|solve_typing|]. Qed.
 
   Lemma type_memcpy_iris E qE L qL tid ty ty1 ty1' ty2 ty2' (n : Z) p1 p2 :
     Z.of_nat (ty.(ty_size)) = n →
@@ -280,9 +285,7 @@ Section typing_rules.
     typed_write E L ty1 ty ty1' →
     typed_read E L ty2 ty ty2' →
     Z.of_nat (ty.(ty_size)) = n →
-    typed_body E L C ((p1 ◁ ty1') :: (p2 ◁ ty2') :: T') e →
+    typed_body E L C ((p1 ◁ ty1') :: (p2 ◁ ty2') :: T') e -∗
     typed_body E L C T (p1 <-{n} !p2;; e).
-  Proof.
-    intros. by eapply type_seq; [|by eapply (type_memcpy_instr ty ty1 ty1')|..].
-  Qed.
+  Proof. iIntros. by iApply type_seq; first eapply (type_memcpy_instr ty ty1 ty1'). Qed.
 End typing_rules.
diff --git a/theories/typing/type_sum.v b/theories/typing/type_sum.v
index 1cc5221c5ccbaa5ff2c00b15ee36b786b02f2df5..e59eee2d3c05c3765260b28f246f7bbcb380e56f 100644
--- a/theories/typing/type_sum.v
+++ b/theories/typing/type_sum.v
@@ -7,6 +7,7 @@ Set Default Proof Using "Type".
 Section case.
   Context `{typeG Σ}.
 
+  (* FIXME : have a iris version of Forall2. *)
   Lemma type_case_own' E L C T p n tyl el :
     Forall2 (λ ty e,
       typed_body E L C ((p +ₗ #0 ◁ own_ptr n (uninit 1)) :: (p +ₗ #1 ◁ own_ptr n ty) ::
@@ -172,11 +173,11 @@ Section case.
     tctx_extract_ctx E L [p1 ◁ ty1; p2 ◁ ty] T T' →
     tyl !! (Z.to_nat i) = Some ty →
     typed_write E L ty1 (sum tyl) ty1' →
-    typed_body E L C ((p1 ◁ ty1') :: T') e →
+    typed_body E L C ((p1 ◁ ty1') :: T') e -∗
     typed_body E L C T (p1 <-{Σ i} p2 ;; e).
   Proof.
-    intros. rewrite -(Z2Nat.id i) //.
-    eapply type_seq; [done|by eapply type_sum_assign_instr|done|done].
+    iIntros. rewrite -(Z2Nat.id i) //.
+    iApply type_seq; [by eapply type_sum_assign_instr|done|done].
   Qed.
 
   Lemma type_sum_assign_unit_instr {E L} (i : nat) tyl ty1 ty2 p :
@@ -200,11 +201,11 @@ Section case.
     tctx_extract_hasty E L p ty1 T T' →
     tyl !! (Z.to_nat i) = Some unit →
     typed_write E L ty1 (sum tyl) ty1' →
-    typed_body E L C ((p ◁ ty1') :: T') e →
+    typed_body E L C ((p ◁ ty1') :: T') e -∗
     typed_body E L C T (p <-{Σ i} () ;; e).
   Proof.
-    intros. rewrite -(Z2Nat.id i) //.
-    eapply type_seq; [done|by eapply type_sum_assign_unit_instr|solve_typing|done].
+    iIntros. rewrite -(Z2Nat.id i) //.
+    iApply type_seq; [by eapply type_sum_assign_unit_instr|solve_typing|done].
   Qed.
 
   Lemma type_sum_memcpy_instr {E L} (i : nat) tyl ty1 ty1' ty2 ty2' ty p1 p2 :
@@ -252,10 +253,10 @@ Section case.
     typed_write E L ty1 (sum tyl) ty1' →
     typed_read E L ty2 ty ty2' →
     Z.of_nat (ty.(ty_size)) = n →
-    typed_body E L C ((p1 ◁ ty1') :: (p2 ◁ ty2') :: T') e →
+    typed_body E L C ((p1 ◁ ty1') :: (p2 ◁ ty2') :: T') e -∗
     typed_body E L C T (p1 <-{n,Σ i} !p2 ;; e).
   Proof.
-    intros ????? Hr ??. subst. rewrite -(Z2Nat.id i) //.
-    by eapply type_seq; [done|eapply type_sum_memcpy_instr, Hr|done|done].
+    iIntros (????? Hr ?) "?". subst. rewrite -(Z2Nat.id i) //.
+    by iApply type_seq; [eapply type_sum_memcpy_instr, Hr|done|done].
   Qed.
 End case.
diff --git a/theories/typing/unsafe/cell.v b/theories/typing/unsafe/cell.v
index 2bcbc1906370a38801102528fdf5c82f2bf23850..ffce1f6b7fef24ed7439939b09ab62c0eee6f478 100644
--- a/theories/typing/unsafe/cell.v
+++ b/theories/typing/unsafe/cell.v
@@ -85,8 +85,8 @@ Section typing.
     typed_instruction_ty [] [] [] cell_new
         (fn([]; ty) → cell ty).
   Proof.
-    eapply type_fn; [solve_typing..|]=>- /= _ ret arg. inv_vec arg=>x. simpl_subst.
-    eapply (type_jump [_]); first solve_typing.
+    iApply type_fn; [solve_typing..|]. simpl. iIntros (_ ret arg). inv_vec arg=>x. simpl_subst.
+    iApply (type_jump [_]); first solve_typing.
     iIntros (???) "#LFT $ $ Hty". rewrite !tctx_interp_singleton /=. done.
   Qed.
 
@@ -97,8 +97,8 @@ Section typing.
     typed_instruction_ty [] [] [] cell_into_inner
         (fn([]; cell ty) → ty).
   Proof.
-    eapply type_fn; [solve_typing..|]=>-/= _ ret arg. inv_vec arg=>x. simpl_subst.
-    eapply (type_jump [_]); first solve_typing.
+    iApply type_fn; [solve_typing..|]. simpl. iIntros (_ ret arg). inv_vec arg=>x. simpl_subst.
+    iApply (type_jump [_]); first solve_typing.
     iIntros (???) "#LFT $ $ Hty". rewrite !tctx_interp_singleton /=. done.
   Qed.
 
@@ -109,8 +109,8 @@ Section typing.
     typed_instruction_ty [] [] [] cell_get_mut
       (fn(∀ α, [☀α]; &uniq{α} (cell ty)) → &uniq{α} ty).
   Proof.
-    eapply type_fn; [solve_typing..|]=>- /= α ret arg. inv_vec arg=>x. simpl_subst.
-    eapply (type_jump [_]). solve_typing. rewrite /tctx_incl /=.
+    iApply type_fn; [solve_typing..|]. simpl. iIntros (α ret arg). inv_vec arg=>x. simpl_subst.
+    iApply (type_jump [_]). solve_typing. rewrite /tctx_incl /=.
     iIntros (???) "_ $$". rewrite !tctx_interp_singleton /tctx_elt_interp /=.
     by iIntros "$".
   Qed.
@@ -126,12 +126,12 @@ Section typing.
     typed_instruction_ty [] [] [] (cell_get ty)
         (fn(∀ α, [☀α]; &shr{α} (cell ty)) → ty).
   Proof.
-    eapply type_fn; [solve_typing..|]=>- /= α ret arg. inv_vec arg=>x. simpl_subst.
-    eapply type_deref; [solve_typing..|apply read_own_move|done|]=>x'. simpl_subst.
-    eapply type_letalloc_n; [solve_typing..| |intros r; simpl_subst].
+    iApply type_fn; [solve_typing..|]. simpl. iIntros (α ret arg). inv_vec arg=>x. simpl_subst.
+    iApply type_deref; [solve_typing|apply read_own_move|done|]. iIntros (x'). simpl_subst.
+    iApply type_letalloc_n; [solve_typing| |iIntros (r); simpl_subst].
     { apply (read_shr _ _ _ (cell ty)); solve_typing. }
-    eapply type_delete; [solve_typing..|].
-    eapply (type_jump [_]); solve_typing.
+    iApply type_delete; [solve_typing..|].
+    iApply (type_jump [_]); solve_typing.
   Qed.
 
   (* Writing to a cell *)
@@ -146,9 +146,9 @@ Section typing.
     typed_instruction_ty [] [] [] (cell_replace ty)
         (fn(∀ α, [☀α]; &shr{α} cell ty, ty) → ty).
   Proof.
-    eapply type_fn; [solve_typing..|]=>- /= α ret arg. inv_vec arg=>c x. simpl_subst.
-    eapply type_deref; [solve_typing..|exact: read_own_move|done|]=> c'; simpl_subst.
-    eapply type_new; [solve_typing..|]=> r; simpl_subst.
+    iApply type_fn; [solve_typing..|]. simpl. iIntros (α ret arg). inv_vec arg=>c x. simpl_subst.
+    iApply type_deref; [solve_typing|exact: read_own_move|done|]. iIntros (c'); simpl_subst.
+    iApply type_new; [solve_typing..|]. iIntros (r); simpl_subst.
     (* Drop to Iris level. *)
     iAlways. iIntros (tid qE) "#LFT Htl HE HL HC".
     rewrite 3!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
@@ -175,15 +175,17 @@ Section typing.
     iMod ("Hclose" with "[Hc'↦ Hxown] Htl") as "[HE Htl]".
     { iExists _. iFrame. }
     (* Now go back to typing level. *)
-    iApply (type_type [☀α]%EL [] _ [c ◁ box (uninit 1); #x ◁ box (uninit ty.(ty_size)); #r ◁ box ty]%TC with "LFT Htl [HE] HL HC"); last first.
+    iApply (type_type _ _ _
+           [c ◁ box (uninit 1); #x ◁ box (uninit ty.(ty_size)); #r ◁ box ty]%TC
+    with "[] LFT Htl [HE] HL HC"); last first.
     { rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
       iFrame "Hc". rewrite !tctx_hasty_val' //. iSplitL "Hx↦ Hx†".
       - iFrame. iExists _. iFrame. iNext. iApply uninit_own. done.
       - iFrame. iExists _. iFrame. }
     { rewrite /elctx_interp big_opL_singleton. done. }
-    eapply type_delete; [solve_typing..|].
-    eapply type_delete; [solve_typing..|].
-    eapply (type_jump [ #_]); solve_typing.
+    iApply type_delete; [solve_typing..|].
+    iApply type_delete; [solve_typing..|].
+    iApply (type_jump [ #_]); solve_typing.
   Qed.
 End typing.
 
diff --git a/theories/typing/unsafe/refcell/ref_code.v b/theories/typing/unsafe/refcell/ref_code.v
index fc845d10a8f6958f0653d84690c9c46aa1b1edd8..bb3cfaab915aaa8ded202b9075ec8de515e530c1 100644
--- a/theories/typing/unsafe/refcell/ref_code.v
+++ b/theories/typing/unsafe/refcell/ref_code.v
@@ -59,8 +59,8 @@ Section ref_functions.
       (fn (fun '(α, β) => [☀α; ☀β])%EL (fun '(α, β) => [# &shr{α}(ref β ty)]%T)
                                        (fun '(α, β) => ref β ty)%T).
   Proof.
-    eapply type_fn; [solve_typing..|]. move=>/= [α β] ret arg. inv_vec arg=>x. simpl_subst.
-    eapply type_deref; [solve_typing..|by apply read_own_move|done|]=>x'.
+    iApply type_fn; [solve_typing..|]. simpl. iIntros ([α β] ret arg). inv_vec arg=>x. simpl_subst.
+    iApply type_deref; [solve_typing..|by apply read_own_move|done|]. iIntros (x').
     iIntros "!# * #LFT Hna HE HL Hk HT". simpl_subst.
     rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
     iDestruct "HT" as "[Hx Hx']". destruct x' as [[|lx'|]|]; try done.
@@ -95,20 +95,17 @@ Section ref_functions.
       - iExists _. iFrame.
         rewrite (comm Qp_plus) (assoc Qp_plus) Qp_div_2 (comm Qp_plus). auto. }
     iMod ("Hcloseβ" with "Hδ") as "Hβ". iMod ("Hcloseα1" with "[$H↦]") as "Hα1".
-    iAssert (elctx_interp [☀ α; ☀ β] qE) with "[Hα1 Hα2 Hβ]" as "HE".
-    { rewrite /elctx_interp big_sepL_cons big_sepL_singleton. iFrame. }
     iApply (type_type _ _ _
-        [ x ◁ box (uninit 1); #lr ◁ box(ref β ty)]%TC with "LFT Hna HE HL Hk");
+        [ x ◁ box (uninit 1); #lr ◁ box(ref β ty)]%TC with "[] LFT Hna [Hα1 Hα2 Hβ] HL Hk");
         first last.
     { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
       rewrite /= freeable_sz_full. iFrame. iExists _. iFrame. iExists _, _, _, _, _.
       iFrame "∗#". }
-    eapply type_delete; [solve_typing..|].
-    eapply (type_jump [ #_]); solve_typing.
+    { rewrite /elctx_interp big_sepL_cons big_sepL_singleton. iFrame. }
+    iApply type_delete; [solve_typing..|].
+    iApply (type_jump [ #_]); solve_typing.
   Qed.
 
-  (* TODO : map, when we will have a nice story about closures. *)
-
   (* Turning a ref into a shared borrow. *)
   Definition ref_deref : val :=
     funrec: <> ["x"] :=
@@ -123,8 +120,8 @@ Section ref_functions.
           (fun '(α, β) => [# &shr{α}(ref β ty)]%T)
           (fun '(α, β) => &shr{α}ty)%T).
   Proof.
-    eapply type_fn; [solve_typing..|]. move=>/= [α β] ret arg. inv_vec arg=>x. simpl_subst.
-    eapply type_deref; [solve_typing..|by apply read_own_move|done|]=>x'.
+    iApply type_fn; [solve_typing..|]. simpl. iIntros ([α β] ret arg). inv_vec arg=>x. simpl_subst.
+    iApply type_deref; [solve_typing..|by apply read_own_move|done|]. iIntros (x').
     iIntros "!# * #LFT Hna HE HL Hk HT". simpl_subst.
     rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
     iDestruct "HT" as "[Hx Hx']". destruct x' as [[|lx'|]|]; try done.
@@ -135,15 +132,15 @@ Section ref_functions.
     rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton.
     iMod "H↦" as "[H↦1 H↦2]". wp_read. wp_let.
     iMod ("Hcloseα" with "[$H↦1 $H↦2]") as "Hα".
-    iAssert (elctx_interp [☀ α; ☀ β; α ⊑ β] qE) with "[Hα Hβ Hαβ]" as "HE".
-    { rewrite /elctx_interp 2!big_sepL_cons big_sepL_singleton. by iFrame. }
     iApply (type_type _ _ _
-        [ x ◁ box (uninit 1); #lv ◁ &shr{α}ty]%TC with "LFT Hna HE HL Hk"); first last.
+        [ x ◁ box (uninit 1); #lv ◁ &shr{α}ty]%TC with "[] LFT Hna [Hα Hβ Hαβ] HL Hk");
+      first last.
     { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
       iFrame. iApply (ty_shr_mono with "LFT [] Hshr"). by iApply lft_incl_glb. }
-    eapply (type_letalloc_1 (&shr{α}ty)); [solve_typing..|].
-    intros r. simpl_subst. eapply type_delete; [solve_typing..|].
-    eapply (type_jump [_]); solve_typing.
+    { rewrite /elctx_interp 2!big_sepL_cons big_sepL_singleton. by iFrame. }
+    iApply (type_letalloc_1 (&shr{α}ty)); [solve_typing..|].
+    iIntros (r). simpl_subst. iApply type_delete; [solve_typing..|].
+    iApply (type_jump [_]); solve_typing.
   Qed.
 
   (* Dropping a ref and decrement the count in the corresponding refcell. *)
@@ -157,10 +154,9 @@ Section ref_functions.
       let: "r" := new [ #0] in "return" ["r"].
 
   Lemma ref_drop_type ty :
-    typed_instruction_ty [] [] [] ref_drop
-      (fn (fun α => [☀α])%EL (fun α => [# ref α ty])  (fun α => unit)).
+    typed_instruction_ty [] [] [] ref_drop (fn(∀ α, [☀α]; ref α ty) → unit).
   Proof.
-    eapply type_fn; [solve_typing..|]=>- /= α ret arg. inv_vec arg=>x. simpl_subst.
+    iApply type_fn; [solve_typing..|]. simpl. iIntros (α ret arg). inv_vec arg=>x. simpl_subst.
     iIntros "!# * #LFT Hna Hα HL Hk Hx".
     rewrite {1}/elctx_interp big_sepL_singleton tctx_interp_singleton tctx_hasty_val.
     destruct x as [[|lx|]|]; try done. iDestruct "Hx" as "[Hx Hx†]".
@@ -196,14 +192,13 @@ Section ref_functions.
     wp_bind Endlft. iApply (wp_fupd_step with "INV"); [done..|]. wp_seq.
     iIntros "INV !>". wp_seq. iMod ("Hcloseβ" with "[$INV] Hna") as "[Hβ Hna]".
     iMod ("Hcloseα" with "Hβ") as "Hα".
-    iAssert (elctx_interp [☀ α] qE) with "[Hα]" as "HE".
-    { by rewrite /elctx_interp big_sepL_singleton. }
-    iApply (type_type _ _ _ [ #lx ◁ box (uninit 2)]%TC with "LFT Hna HE HL Hk");
+    iApply (type_type _ _ _ [ #lx ◁ box (uninit 2)]%TC with "[] LFT Hna [Hα] HL Hk");
       first last.
     { rewrite tctx_interp_singleton tctx_hasty_val' //. iFrame. iExists [ #lv;#lrc].
       rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton uninit_own. iFrame. auto. }
-    eapply type_delete; [solve_typing..|].
-    eapply type_new; [solve_typing..|]=>r. simpl_subst.
-    eapply (type_jump [_]); solve_typing.
+    { by rewrite /elctx_interp big_sepL_singleton. }
+    iApply type_delete; [solve_typing..|].
+    iApply type_new; [solve_typing..|]. iIntros (r). simpl_subst.
+    iApply (type_jump [_]); solve_typing.
   Qed.
 End ref_functions.
diff --git a/theories/typing/unsafe/refcell/refcell_code.v b/theories/typing/unsafe/refcell/refcell_code.v
index 53185ea835ba4f9972b0b89b391c6548f9e9bf88..9fe6fa40cfe96ed54591092dc794f93bcead690c 100644
--- a/theories/typing/unsafe/refcell/refcell_code.v
+++ b/theories/typing/unsafe/refcell/refcell_code.v
@@ -23,8 +23,8 @@ Section refcell_functions.
     typed_instruction_ty [] [] [] (refcell_new ty)
         (fn (λ _, []) (λ _, [# ty]) (λ _:(), refcell ty)).
   Proof.
-    eapply type_fn; [solve_typing..|]=>-/= _ ret arg. inv_vec arg=>x. simpl_subst.
-    eapply type_new; [solve_typing..|].
+    iApply type_fn; [solve_typing..|]. simpl. iIntros (_ ret arg). inv_vec arg=>x. simpl_subst.
+    iApply type_new; [solve_typing..|].
     iIntros (r) "!# * #LFT Hna HE HL Hk HT". simpl_subst.
     rewrite (Nat2Z.id (S ty.(ty_size))) tctx_interp_cons
             tctx_interp_singleton !tctx_hasty_val.
@@ -38,13 +38,13 @@ Section refcell_functions.
     wp_apply (wp_memcpy with "[$Hr↦1 $Hx↦]"); [done||lia..|].
     iIntros "[Hr↦1 Hx↦]". wp_seq.
     iApply (type_type _ _ _ [ #lx ◁ box (uninit (ty_size ty)); #lr ◁ box (refcell ty)]%TC
-        with "LFT Hna HE HL Hk [-]"); last first.
+        with "[] LFT Hna HE HL Hk [-]"); last first.
     { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val' //=. iFrame.
       iSplitL "Hx↦".
       - iExists _. rewrite uninit_own. auto.
       - iExists (_::_). rewrite heap_mapsto_vec_cons. iFrame. auto. }
-    eapply type_delete; [solve_typing..|].
-    eapply (type_jump [ #_]); solve_typing.
+    iApply type_delete; [solve_typing..|].
+    iApply (type_jump [ #_]); solve_typing.
   Qed.
 
   (* The other direction: getting ownership out of a refcell. *)
@@ -60,8 +60,8 @@ Section refcell_functions.
     typed_instruction_ty [] [] [] (refcell_into_inner ty)
         (fn (λ _, []) (λ _, [# refcell ty]) (λ _:(), ty)).
   Proof.
-    eapply type_fn; [solve_typing..|]=>- /= _ ret arg. inv_vec arg=>x. simpl_subst.
-    eapply type_new; [solve_typing..|].
+    iApply type_fn; [solve_typing..|]. simpl. iIntros (_ ret arg). inv_vec arg=>x. simpl_subst.
+    iApply type_new; [solve_typing..|].
     iIntros (r) "!# * #LFT Hna HE HL Hk HT". simpl_subst.
     rewrite (Nat2Z.id (ty.(ty_size))) tctx_interp_cons
             tctx_interp_singleton !tctx_hasty_val.
@@ -75,13 +75,13 @@ Section refcell_functions.
     wp_apply (wp_memcpy with "[$Hr↦ $Hx↦1]"); [done||lia..|].
     iIntros "[Hr↦ Hx↦1]". wp_seq.
     iApply (type_type _ _ _ [ #lx ◁ box (uninit (S (ty_size ty))); #lr ◁ box ty]%TC
-        with "LFT Hna HE HL Hk [-]"); last first.
+        with "[] LFT Hna HE HL Hk [-]"); last first.
     { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val' //. iFrame.
       iSplitR "Hr↦ Hx".
       - iExists (_::_). rewrite heap_mapsto_vec_cons uninit_own -Hsz. iFrame. auto.
       - iExists vl. iFrame. }
-    eapply type_delete; [solve_typing..|].
-    eapply (type_jump [ #_]); solve_typing.
+    iApply type_delete; [solve_typing..|].
+    iApply (type_jump [ #_]); solve_typing.
   Qed.
 
   Definition refcell_get_mut : val :=
@@ -94,8 +94,8 @@ Section refcell_functions.
     typed_instruction_ty [] [] [] refcell_get_mut
         (fn (λ α, [☀α])%EL (λ α, [# &uniq{α} (refcell ty)])%T (λ α, &uniq{α} ty)%T).
   Proof.
-    eapply type_fn; [solve_typing..|]=>- /= α ret arg. inv_vec arg=>x. simpl_subst.
-    eapply type_deref; [solve_typing..|by eapply read_own_move|done|]=>x'. simpl_subst.
+    iApply type_fn; [solve_typing..|]. simpl. iIntros (α ret arg). inv_vec arg=>x. simpl_subst.
+    iApply type_deref; [solve_typing..|by eapply read_own_move|done|]. iIntros (x'). simpl_subst.
     iIntros "!# * #LFT Hna HE HL HC HT".
     rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
     iDestruct "HT" as "[Hx Hx']". destruct x' as [[|lx'|]|];  try iDestruct "Hx'" as "[]".
@@ -112,11 +112,11 @@ Section refcell_functions.
     iDestruct "Hx" as (vl) "[Hx↦ Hx]". rewrite uninit_own. wp_op.
     iApply (type_type _ _ _
             [ #lx ◁ box (uninit 1); #(shift_loc lx' 1) ◁ &uniq{α}ty]%TC
-            with "LFT Hna HE HL HC [-]"); last first.
+            with "[] LFT Hna HE HL HC [-]"); last first.
     { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val' //. iFrame.
       iNext. iExists _. rewrite uninit_own. iFrame. }
-    eapply type_assign; [solve_typing..|exact: write_own|].
-    eapply (type_jump [ #_]); solve_typing.
+    iApply type_assign; [solve_typing..|exact: write_own|].
+    iApply (type_jump [ #_]); solve_typing.
   Qed.
 
   (* Shared borrowing. *)
@@ -143,14 +143,14 @@ Section refcell_functions.
     typed_instruction_ty [] [] [] refcell_try_borrow
         (fn (λ α, [☀α])%EL (λ α, [# &shr{α}(refcell ty)]%T) (λ α, Σ[ref α ty; unit])%T).
   Proof.
-    eapply type_fn; [solve_typing..|]=>- /= α ret arg. inv_vec arg=>x. simpl_subst.
-    eapply (type_cont [_] [] (λ r, [x ◁ box (&shr{α} refcell ty);
+    iApply type_fn; [solve_typing..|]. simpl. iIntros (α ret arg). inv_vec arg=>x. simpl_subst.
+    iApply (type_cont [_] [] (λ r, [x ◁ box (&shr{α} refcell ty);
                                     r!!!0 ◁ box Σ[ref α ty; unit]])%TC);
-      [solve_typing..|intros k|move=>/= k arg; inv_vec arg=>r]; simpl_subst; last first.
-    { eapply type_delete; [solve_typing..|].
-      eapply (type_jump [_]); solve_typing. }
-    eapply type_new; [solve_typing..|]=>r. simpl_subst.
-    eapply type_deref; [solve_typing..|apply read_own_copy, _|done|].
+      [iIntros (k)|simpl; iIntros (k arg); inv_vec arg=>r]; simpl_subst; last first.
+    { iApply type_delete; [solve_typing..|].
+      iApply (type_jump [_]); solve_typing. }
+    iApply type_new; [solve_typing..|]. iIntros (r). simpl_subst.
+    iApply type_deref; [solve_typing..|apply read_own_copy, _|done|].
     iIntros (x') "!# * #LFT Hna HE HL Hk HT". simpl_subst.
     rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
     iDestruct "HT" as "(Hx & Hx' & Hr)". destruct x' as [[|lx|]|]; try done.
@@ -161,15 +161,14 @@ Section refcell_functions.
     iDestruct "INV" as (st) "(Hlx & Hownst & Hst)". wp_read. wp_let. wp_op=>?; wp_if.
     - iMod ("Hclose'" with "[Hlx Hownst Hst] Hna") as "[Hβtok1 Hna]";
         first by iExists st; iFrame.
-      iAssert (elctx_interp [☀α] qE)%I with ">[Hclose Hβtok1 Hβtok2]" as "HE".
-      { rewrite {1}/elctx_interp big_sepL_singleton /=. iApply "Hclose". by iFrame. }
       iApply (type_type _ _ _
               [ x ◁ box (&shr{α}(refcell ty)); r ◁ box (uninit 3) ]%TC
-              with "LFT Hna HE HL Hk"); first last.
+              with "[] LFT Hna >[Hclose Hβtok1 Hβtok2] HL Hk"); first last.
       { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val. iFrame. }
-      eapply (type_sum_assign_unit [ref α ty; unit]);
+      { rewrite {1}/elctx_interp big_sepL_singleton /=. iApply "Hclose". by iFrame. }
+      iApply (type_sum_assign_unit [ref α ty; unit]);
         [solve_typing..|by eapply write_own|]; first last.
-      simpl. eapply (type_jump [_]); solve_typing.
+      simpl. iApply (type_jump [_]); solve_typing.
     - wp_op. wp_write. wp_apply wp_new; [done..|].
       iIntros (lref vl) "(EQ & H† & Hlref)". iDestruct "EQ" as %?%(inj Z.of_nat 2%nat).
       destruct vl as [|?[|?[]]]; try done. wp_let.
@@ -209,20 +208,20 @@ Section refcell_functions.
             iNext. iMod "Hν". iApply "Hh". rewrite -lft_dead_or. auto.
           + iExists _. iFrame. by rewrite Qp_div_2. }
       iMod ("Hclose'" with "[$INV] Hna") as "[Hβtok1 Hna]".
-      iAssert (elctx_interp [☀α] qE)%I with ">[Hclose Hβtok1 Hβtok2]" as "HE".
-      { rewrite {1}/elctx_interp big_sepL_singleton /=. iApply "Hclose". by iFrame. }
       iApply (type_type  _ _ _
         [ x ◁ box (&shr{α}(refcell ty)); r ◁ box (uninit 3); #lref ◁ box (ref α ty)]%TC
-              with "LFT Hna HE HL Hk");
+              with "[] LFT Hna >[Hclose Hβtok1 Hβtok2] HL Hk");
         first last.
       { rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val. iFrame.
         rewrite tctx_hasty_val' //. rewrite /= freeable_sz_full. iFrame.
         iExists [_; _]. rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton.
         iFrame. iExists _, _, _, _, _. iFrame "∗#". iApply ty_shr_mono; try by auto.
         iApply lft_glb_mono. done. iApply lft_incl_refl. }
-      eapply (type_sum_memcpy [ref α ty; unit]);
+      { rewrite {1}/elctx_interp big_sepL_singleton /=. iApply "Hclose". by iFrame. }
+      iApply (type_sum_memcpy [ref α ty; unit]);
         [solve_typing..|by eapply write_own|by eapply read_own_move|done|].
-      simpl. eapply type_delete; [solve_typing..|]. eapply (type_jump [_]); solve_typing.
+      simpl. iApply type_delete; [solve_typing..|].
+      iApply (type_jump [_]); solve_typing.
   Qed.
 
   (* Unique borrowing. *)
@@ -249,14 +248,14 @@ Section refcell_functions.
     typed_instruction_ty [] [] [] refcell_try_borrow_mut
         (fn (λ α, [☀α])%EL (λ α, [# &shr{α}(refcell ty)]%T) (λ α, Σ[refmut α ty; unit])%T).
   Proof.
-    eapply type_fn; [solve_typing..|]=>- /= α ret arg. inv_vec arg=>x. simpl_subst.
-    eapply (type_cont [_] [] (λ r, [x ◁ box (&shr{α} refcell ty);
+    iApply type_fn; [solve_typing..|]. simpl. iIntros (α ret arg). inv_vec arg=>x. simpl_subst.
+    iApply (type_cont [_] [] (λ r, [x ◁ box (&shr{α} refcell ty);
                                     r!!!0 ◁ box Σ[refmut α ty; unit]])%TC);
-      [solve_typing..|intros k|move=>/= k arg; inv_vec arg=>r]; simpl_subst; last first.
-    { eapply type_delete; [solve_typing..|].
-      eapply (type_jump [_]); solve_typing. }
-    eapply type_new; [solve_typing..|]=>r. simpl_subst.
-    eapply type_deref; [solve_typing..|apply read_own_copy, _|done|].
+      [iIntros (k)|simpl; iIntros (k arg); inv_vec arg=>r]; simpl_subst; last first.
+    { iApply type_delete; [solve_typing..|].
+      iApply (type_jump [_]); solve_typing. }
+    iApply type_new; [solve_typing..|]. iIntros (r). simpl_subst.
+    iApply type_deref; [solve_typing..|apply read_own_copy, _|done|].
     iIntros (x') "!# * #LFT Hna HE HL Hk HT". simpl_subst.
     rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
     iDestruct "HT" as "(Hx & Hx' & Hr)". destruct x' as [[|lx|]|]; try done.
@@ -280,29 +279,28 @@ Section refcell_functions.
       { iExists _. iFrame. iExists ν. iSplit; first by auto. iNext. iSplitL; last by auto.
         iIntros "Hν". iMod ("Hhν" with "Hν") as "Hν". iModIntro. iNext. iMod "Hν".
         iApply "Hbh". rewrite -lft_dead_or. auto. }
-      iAssert (elctx_interp [☀α] qE)%I with ">[Hclose Hβtok]" as "HE".
-      { rewrite {1}/elctx_interp big_sepL_singleton /=. iApply "Hclose". by iFrame. }
       iApply (type_type _ _ _
         [ x ◁ box (&shr{α}(refcell ty)); r ◁ box (uninit 3); #lref ◁ box (refmut α ty)]%TC
-              with "LFT Hna HE HL Hk"); first last.
+              with "[] LFT Hna >[Hclose Hβtok] HL Hk"); first last.
       { rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val. iFrame.
         rewrite tctx_hasty_val' //. rewrite /= freeable_sz_full. iFrame.
         iExists [_; _]. rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton.
         iFrame. iExists _, _, _, _. iFrame "#∗". iApply (bor_shorten with "[] [$Hb]").
         iApply lft_glb_mono; first done. iApply lft_incl_refl. }
-      eapply (type_sum_memcpy [refmut α ty; unit]);
+      { rewrite {1}/elctx_interp big_sepL_singleton /=. iApply "Hclose". by iFrame. }
+      iApply (type_sum_memcpy [refmut α ty; unit]);
         [solve_typing..|by eapply write_own|by eapply read_own_move|done|].
-      simpl. eapply type_delete; [solve_typing..|]. eapply (type_jump [_]); solve_typing.
+      simpl. iApply type_delete; [solve_typing..|].
+      iApply (type_jump [_]); solve_typing.
     - iMod ("Hclose'" with "[Hlx Hownst Hb] Hna") as "[Hβtok Hna]";
         first by iExists st; iFrame.
-      iAssert (elctx_interp [☀α] qE)%I with ">[Hclose Hβtok]" as "HE".
-      { rewrite {1}/elctx_interp big_sepL_singleton /=. iApply "Hclose". by iFrame. }
       iApply (type_type _ _ _
               [ x ◁ box (&shr{α}(refcell ty)); r ◁ box (uninit 3) ]%TC
-              with "LFT Hna HE HL Hk"); first last.
+              with "[] LFT Hna >[Hclose Hβtok] HL Hk"); first last.
       { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val. iFrame. }
-      eapply (type_sum_assign_unit [refmut α ty; unit]);
+      { rewrite {1}/elctx_interp big_sepL_singleton /=. iApply "Hclose". by iFrame. }
+      iApply (type_sum_assign_unit [refmut α ty; unit]);
         [solve_typing..|by eapply write_own|].
-      simpl. eapply (type_jump [_]); solve_typing.
+      simpl. iApply (type_jump [_]); solve_typing.
   Qed.
 End refcell_functions.
diff --git a/theories/typing/unsafe/refcell/refmut_code.v b/theories/typing/unsafe/refcell/refmut_code.v
index cfb17aa0fc62803aa344d9db69ec57056f9a97f8..8f9bd7483d472637f48b0a02207b928e940f989d 100644
--- a/theories/typing/unsafe/refcell/refmut_code.v
+++ b/theories/typing/unsafe/refcell/refmut_code.v
@@ -26,8 +26,8 @@ Section refmut_functions.
           (fun '(α, β) => [# &shr{α}(refmut β ty)]%T)
           (fun '(α, β) => &shr{α}ty)%T).
   Proof.
-    eapply type_fn; [solve_typing..|]. move=> /= [α β] ret arg. inv_vec arg=>x. simpl_subst.
-    eapply type_deref; [solve_typing..|by apply read_own_move|done|]=>x'.
+    iApply type_fn; [solve_typing..|]. simpl. iIntros ([α β] ret arg). inv_vec arg=>x. simpl_subst.
+    iApply type_deref; [solve_typing..|by apply read_own_move|done|]. iIntros (x').
     iIntros "!# * #LFT Hna HE HL Hk HT". simpl_subst.
     rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
     iDestruct "HT" as "[Hx Hx']". destruct x' as [[|lx'|]|]; try done.
@@ -42,15 +42,15 @@ Section refmut_functions.
     iMod "H↦" as "[H↦1 H↦2]". wp_read. iIntros "[#Hshr' Hα2β]!>". wp_let.
     iDestruct ("Hcloseβα2" with "Hα2β") as "[Hβ Hα2]".
     iMod ("Hcloseα1" with "[$H↦1 $H↦2]") as "Hα1".
-    iApply (type_type [☀ α; ☀ β; α ⊑ β]%EL _ _ [ x ◁ box (uninit 1); #lv ◁ &shr{α}ty]%TC
-            with "LFT Hna [Hα1 Hα2 Hβ Hαβ] HL Hk"); last first.
+    iApply (type_type _ _ _ [ x ◁ box (uninit 1); #lv ◁ &shr{α}ty]%TC
+            with "[] LFT Hna [Hα1 Hα2 Hβ Hαβ] HL Hk"); last first.
     { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
       iFrame. iApply (ty_shr_mono with "LFT [] Hshr'"). iApply lft_incl_glb; first done.
       iApply lft_incl_refl. }
     { rewrite /elctx_interp 2!big_sepL_cons big_sepL_singleton. by iFrame. }
-    eapply (type_letalloc_1 (&shr{α}ty)); [solve_typing..|].
-    intros r. simpl_subst. eapply type_delete; [solve_typing..|].
-    eapply (type_jump [_]); solve_typing.
+    iApply (type_letalloc_1 (&shr{α}ty)); [solve_typing..|].
+    iIntros (r). simpl_subst. iApply type_delete; [solve_typing..|].
+    iApply (type_jump [_]); solve_typing.
   Qed.
 
   (* Turning a refmut into a unique borrow. *)
@@ -67,8 +67,8 @@ Section refmut_functions.
           (fun '(α, β) => [# &uniq{α}(refmut β ty)]%T)
           (fun '(α, β) => &uniq{α}ty)%T).
   Proof.
-    eapply type_fn; [solve_typing..|]. move=>/= [α β] ret arg. inv_vec arg=>x. simpl_subst.
-    eapply type_deref; [solve_typing..|by apply read_own_move|done|]=>x'.
+    iApply type_fn; [solve_typing..|]. simpl. iIntros ([α β] ret arg). inv_vec arg=>x. simpl_subst.
+    iApply type_deref; [solve_typing..|by apply read_own_move|done|]. iIntros (x').
     iIntros "!# * #LFT Hna HE HL Hk HT". simpl_subst.
     rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
     iDestruct "HT" as "[Hx Hx']".
@@ -96,15 +96,15 @@ Section refmut_functions.
       [done| |by iApply (bor_unnest with "LFT Hb")|]; first done.
     wp_read. iIntros "Hb !>". wp_let.
     iMod ("Hcloseα" with "[$H↦]") as "[_ Hα]".
-    iApply (type_type [☀ α; ☀ β; α ⊑ β]%EL _ _ [ x ◁ box (uninit 1); #lv ◁ &uniq{α}ty]%TC
-            with "LFT Hna [Hα Hβ Hαβ] HL Hk"); last first.
+    iApply (type_type _ _ _ [ x ◁ box (uninit 1); #lv ◁ &uniq{α}ty]%TC
+            with "[] LFT Hna [Hα Hβ Hαβ] HL Hk"); last first.
     { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
       iFrame. iApply (bor_shorten with "[] Hb").
       by iApply lft_incl_glb; [iApply lft_incl_glb|iApply lft_incl_refl]. }
     { rewrite /elctx_interp 2!big_sepL_cons big_sepL_singleton. by iFrame. }
-    eapply (type_letalloc_1 (&uniq{α}ty)); [solve_typing..|].
-    intros r. simpl_subst. eapply type_delete; [solve_typing..|].
-    eapply (type_jump [_]); solve_typing.
+    iApply (type_letalloc_1 (&uniq{α}ty)); [solve_typing..|].
+    iIntros (r). simpl_subst. iApply type_delete; [solve_typing..|].
+    iApply (type_jump [_]); solve_typing.
   Qed.
 
   (* Dropping a refmut and set the count to 0 in the corresponding refcell. *)
@@ -117,10 +117,9 @@ Section refmut_functions.
       let: "r" := new [ #0] in "return" ["r"].
 
   Lemma refmut_drop_type ty :
-    typed_instruction_ty [] [] [] refmut_drop
-      (fn(∀ α, [☀α]; refmut α ty) → unit).
+    typed_instruction_ty [] [] [] refmut_drop (fn(∀ α, [☀α]; refmut α ty) → unit).
   Proof.
-    eapply type_fn; [solve_typing..|]. move=>/= α ret arg. inv_vec arg=>x. simpl_subst.
+    iApply type_fn; [solve_typing..|]. simpl. iIntros (α ret arg). inv_vec arg=>x. simpl_subst.
     iIntros "!# * #LFT Hna Hα HL Hk Hx".
     rewrite {1}/elctx_interp big_sepL_singleton tctx_interp_singleton tctx_hasty_val.
     destruct x as [[|lx|]|]; try done. iDestruct "Hx" as "[Hx Hx†]".
@@ -145,13 +144,13 @@ Section refmut_functions.
       apply auth_update_dealloc. rewrite -(right_id None _ (Some _)).
       apply cancel_local_update_empty, _. }
     iMod ("Hcloseα" with "Hβ") as "Hα". wp_seq.
-    iApply (type_type [☀ α]%EL _ _ [ #lx ◁ box (uninit 2)]%TC
-            with "LFT Hna [Hα] HL Hk"); last first.
+    iApply (type_type _ _ _ [ #lx ◁ box (uninit 2)]%TC
+            with "[] LFT Hna [Hα] HL Hk"); last first.
     { rewrite tctx_interp_singleton tctx_hasty_val' //. iFrame. iExists [ #lv;#lrc].
       rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton uninit_own. iFrame. auto. }
     { by rewrite /elctx_interp big_sepL_singleton. }
-    eapply type_delete; [solve_typing..|].
-    eapply type_new; [solve_typing..|]=>r. simpl_subst.
-    eapply (type_jump [_]); solve_typing.
+    iApply type_delete; [solve_typing..|].
+    iApply type_new; [solve_typing..|]. iIntros (r). simpl_subst.
+    iApply (type_jump [_]); solve_typing.
   Qed.
 End refmut_functions.
diff --git a/theories/typing/unsafe/spawn.v b/theories/typing/unsafe/spawn.v
index 656a167d7142ddce391170b5dc2d16833daa45b4..9addc231d7fa23cafe62a675d5709d1a52913fd8 100644
--- a/theories/typing/unsafe/spawn.v
+++ b/theories/typing/unsafe/spawn.v
@@ -65,11 +65,11 @@ Section spawn.
     typed_instruction_ty [] [] [] spawn
         (fn([]; fn([] ; envty) → retty, envty) → join_handle retty).
   Proof. (* FIXME: typed_instruction_ty is not used for printing. *)
-    eapply type_fn; [solve_typing..|]=>- _ ret /= arg. inv_vec arg=>f env. simpl_subst.
-    eapply type_deref; [solve_typing..|exact: read_own_move|done|].
-    move=>f'. simpl_subst.
-    eapply type_let with (T1 := [f' ◁ _; env ◁ _]%TC)
-                         (T2 := λ j, [j ◁ join_handle retty]%TC); try solve_typing; [|].
+    iApply type_fn; [solve_typing..|]. simpl. iIntros (_ ret arg). inv_vec arg=>f env. simpl_subst.
+    iApply type_deref; [solve_typing..|exact: read_own_move|done|].
+    iIntros (f'). simpl_subst.
+    iApply (type_let _ _ _ _ ([f' ◁ _; env ◁ _]%TC)
+                     (λ j, [j ◁ join_handle retty]%TC)); try solve_typing; [|].
     { (* The core of the proof: showing that spawn is safe. *)
       iAlways. iIntros (tid qE) "#LFT $ $ $".
       rewrite tctx_interp_cons tctx_interp_singleton.
@@ -96,12 +96,11 @@ Section spawn.
         + rewrite !tctx_hasty_val.
           iApply @send_change_tid. done.
         + rewrite !tctx_hasty_val. iApply @send_change_tid. done. }
-    move=>v. simpl_subst.
-    eapply type_new; [solve_typing..|].
-    intros r. simpl_subst.
-    eapply type_assign; [solve_typing..|exact: write_own|].
-    eapply type_delete; [solve_typing..|].
-    eapply (type_jump [_]); solve_typing.
+    iIntros (v). simpl_subst.
+    iApply type_new; [solve_typing..|]. iIntros (r). simpl_subst.
+    iApply type_assign; [solve_typing..|exact: write_own|].
+    iApply type_delete; [solve_typing..|].
+    iApply (type_jump [_]); solve_typing.
   Qed.
 
   Definition join : val :=
@@ -114,10 +113,10 @@ Section spawn.
     typed_instruction_ty [] [] [] join
         (fn([]; join_handle retty) → retty).
   Proof.
-    eapply type_fn; [solve_typing..|]=>- _ ret /= arg. inv_vec arg=>c. simpl_subst.
-    eapply type_deref; [solve_typing..|exact: read_own_move|done|]. move=>c'; simpl_subst.
-    eapply type_let with (T1 := [c' ◁ _]%TC)
-                         (T2 := λ r, [r ◁ box retty]%TC); try solve_typing; [|].
+    iApply type_fn; [solve_typing..|]. simpl. iIntros (_ ret arg). inv_vec arg=>c. simpl_subst.
+    iApply type_deref; [solve_typing..|exact: read_own_move|done|]. iIntros (c'); simpl_subst.
+    iApply (type_let _ _ _ _ ([c' ◁ _]%TC)
+                             (λ r, [r ◁ box retty]%TC)); try solve_typing; [|].
     { iAlways. iIntros (tid qE) "#LFT $ $ $".
       rewrite tctx_interp_singleton tctx_hasty_val. iIntros "Hc'".
       destruct c' as [[|c'|]|]; try done. iDestruct "Hc'" as (ty') "[#Hsub Hc']".
@@ -126,8 +125,7 @@ Section spawn.
       iPoseProof "Hsub" as "Hsz". iDestruct "Hsz" as "[% _]".
       iDestruct (own_type_incl with "Hsub") as "(_ & Hincl & _)".
       iApply "Hincl". rewrite -H. done. }
-    move=>r; simpl_subst.
-    eapply type_delete; [solve_typing..|].
-    eapply (type_jump [_]); solve_typing.
+    iIntros (r); simpl_subst. iApply type_delete; [solve_typing..|].
+    iApply (type_jump [_]); solve_typing.
   Qed.
 End spawn.