diff --git a/opam b/opam
index e09ae8787b6bb4dd85da880b67a36e7839f5ce0e..78255aafcc49ad72a7501991269185d131dae667 100644
--- a/opam
+++ b/opam
@@ -10,5 +10,5 @@ build: [make "-j%{jobs}%"]
 install: [make "install"]
 remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/lrust'" ]
 depends: [
-  "coq-iris" { (= "dev.2017-09-25.0") | (= "dev") }
+  "coq-iris" { (= "dev.2017-10-19.0") | (= "dev") }
 ]
diff --git a/theories/lang/adequacy.v b/theories/lang/adequacy.v
index 7a401f6139326de8b71cfac97caee71463b056d9..e925d71bc9dc6f4a48889ae11c7bfe3d43c816b7 100644
--- a/theories/lang/adequacy.v
+++ b/theories/lang/adequacy.v
@@ -28,5 +28,5 @@ Proof.
   set (Hheap := HeapG _ _ _ vγ fγ).
   iModIntro. iExists heap_ctx. iSplitL.
   { iExists ∅. by iFrame. }
-  iApply (Hwp (LRustG _ _ Hheap)).
+  by iApply (Hwp (LRustG _ _ Hheap)).
 Qed.
diff --git a/theories/lang/lib/new_delete.v b/theories/lang/lib/new_delete.v
index dfe6bc79bc4bb09c41b0b2a06b7f02e555621689..74da98afbaac84d88d944aa7f2bb2a9bec951588 100644
--- a/theories/lang/lib/new_delete.v
+++ b/theories/lang/lib/new_delete.v
@@ -22,7 +22,7 @@ Section specs.
     {{{ l vl, RET LitV $ LitLoc l;
         ⌜n = length vl⌝ ∗ (†l…(Z.to_nat n) ∨ ⌜n = 0⌝) ∗ l ↦∗ vl }}}.
   Proof.
-    iIntros (? Φ) "HΦ". wp_lam. wp_op; intros ?.
+    iIntros (? Φ) "_ HΦ". wp_lam. wp_op; intros ?.
     - wp_if. assert (n = 0) as -> by lia. iApply ("HΦ" $! _ []).
       rewrite heap_mapsto_vec_nil. auto.
     - wp_if. wp_alloc l vl as "H↦" "H†". iApply ("HΦ" $! _ vl).
diff --git a/theories/lang/lib/spawn.v b/theories/lang/lib/spawn.v
index 34a1ef5269a778f88c62114d868dac7f74b01cfc..96a930b526265ee41583913e5e58de40b02607bf 100644
--- a/theories/lang/lib/spawn.v
+++ b/theories/lang/lib/spawn.v
@@ -108,7 +108,7 @@ Proof.
     - iModIntro. iApply wp_if. iNext. iApply ("IH" with "Hj H†").
       auto. }
   iDestruct "Ho" as (v) "(Hd & HΨ & Hf)".
-  iMod ("Hclose" with "[Hj Hf]").
+  iMod ("Hclose" with "[Hj Hf]") as "_".
   { iNext. iLeft. iFrame. }
   iModIntro. iApply wp_if. iNext. wp_op. wp_read. wp_let.
   iAssert (c ↦∗ [ #true; v])%I with "[Hc Hd]" as "Hc".
diff --git a/theories/lang/lifting.v b/theories/lang/lifting.v
index 40d5c1497041cc8270f2b265b32bf66c41966777..c8b7ad810fe99c80ad1ba9a07e479c20a126268b 100644
--- a/theories/lang/lifting.v
+++ b/theories/lang/lifting.v
@@ -46,7 +46,7 @@ Lemma wp_alloc E (n : Z) :
   {{{ True }}} Alloc (Lit $ LitInt n) @ E
   {{{ l sz (vl : vec val sz), RET LitV $ LitLoc l; ⌜n = sz⌝ ∗ †l…(Z.to_nat n) ∗ l ↦∗ vl }}}.
 Proof.
-  iIntros (? Φ) "HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
+  iIntros (? Φ) "_ HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
   iIntros (σ1) "Hσ !>"; iSplit; first by auto.
   iNext; iIntros (v2 σ2 efs Hstep); inv_head_step.
   iMod (heap_alloc with "Hσ") as "[Hσ Hl]"; [done..|].
@@ -215,7 +215,7 @@ Lemma wp_fork E e :
 Proof.
   iIntros (?) "?HΦ". iApply wp_lift_pure_det_head_step; eauto.
   by intros; inv_head_step; eauto. iApply step_fupd_intro; first done. iNext.
-  rewrite big_sepL_singleton. iFrame. iApply wp_value. done. by iApply "HΦ".
+  rewrite big_sepL_singleton. iFrame. iApply wp_value. by iApply "HΦ".
 Qed.
 
 Lemma wp_rec_step_fupd E E' e f xl erec erec' el Φ :
@@ -245,11 +245,11 @@ Lemma wp_bin_op_pure E op l1 l2 l' :
   {{{ True }}} BinOp op (Lit l1) (Lit l2) @ E
   {{{ l'' σ, RET LitV l''; ⌜bin_op_eval σ op l1 l2 l''⌝ }}}.
 Proof.
-  iIntros (? Φ) "HΦ". iApply wp_lift_pure_head_step; eauto.
+  iIntros (? Φ) "_ HΦ". iApply wp_lift_pure_head_step; eauto.
   { intros. by inv_head_step. }
   iApply step_fupd_intro; first done. iNext. iIntros (e2 efs σ Hs).
   inv_head_step; rewrite right_id.
-  rewrite -wp_value //. iApply "HΦ". eauto.
+  rewrite -wp_value. iApply "HΦ". eauto.
 Qed.
 
 Lemma wp_le E (n1 n2 : Z) P Φ :
@@ -259,7 +259,7 @@ Lemma wp_le E (n1 n2 : Z) P Φ :
 Proof.
   iIntros (Hl Hg) "HP".
   destruct (bool_decide_reflect (n1 ≤ n2)); [rewrite Hl //|rewrite Hg; last omega];
-    clear Hl Hg; (iApply wp_bin_op_pure; first by econstructor); iNext; iIntros (?? Heval);
+    clear Hl Hg; (iApply wp_bin_op_pure; first by econstructor); try done; iNext; iIntros (?? Heval);
     inversion_clear Heval; [rewrite bool_decide_true //|rewrite bool_decide_false //].
 Qed.
 
@@ -270,7 +270,7 @@ Lemma wp_eq_int E (n1 n2 : Z) P Φ :
 Proof.
   iIntros (Heq Hne) "HP".
   destruct (bool_decide_reflect (n1 = n2)); [rewrite Heq //|rewrite Hne //];
-    clear Hne Heq; iApply wp_bin_op_pure; subst.
+    clear Hne Heq; iApply wp_bin_op_pure; subst; try done.
   - intros. apply BinOpEqTrue. constructor.
   - iNext; iIntros (?? Heval). by inversion_clear Heval; inv_lit.
   - intros. apply BinOpEqFalse. by constructor.
@@ -286,7 +286,7 @@ Lemma wp_eq_loc E (l1 : loc) (l2: loc) P Φ :
 Proof.
   iIntros (Hl1 Hl2 Heq Hne) "HP".
   destruct (bool_decide_reflect (l1 = l2)).
-  - rewrite Heq // {Heq Hne}. iApply wp_bin_op_pure; subst.
+  - rewrite Heq // {Heq Hne}. iApply wp_bin_op_pure; subst; try done.
     + intros. apply BinOpEqTrue. constructor.
     + iNext. iIntros (?? Heval). by inversion_clear Heval; inv_lit.
   - clear Heq. iApply wp_lift_atomic_head_step_no_fork; subst=>//.
@@ -320,23 +320,25 @@ Lemma wp_eq_loc_0_r E (l : loc) P Φ :
   (P -∗ ▷ Φ (LitV false)) →
   P -∗ WP BinOp EqOp (Lit (LitLoc l)) (Lit (LitInt 0)) @ E {{ Φ }}.
 Proof.
-  iIntros (HΦ) "HP". iApply wp_bin_op_pure. by intros; do 2 constructor.
-  rewrite HΦ. iNext. iIntros (?? Heval). by inversion_clear Heval; inv_lit.
+  iIntros (HΦ) "HP". iApply wp_bin_op_pure; try done.
+  -  by intros; do 2 constructor.
+  -  rewrite HΦ. iNext. iIntros (?? Heval). by inversion_clear Heval; inv_lit.
 Qed.
 
 Lemma wp_eq_loc_0_l E (l : loc) P Φ :
   (P -∗ ▷ Φ (LitV false)) →
   P -∗ WP BinOp EqOp (Lit (LitInt 0)) (Lit (LitLoc l)) @ E {{ Φ }}.
 Proof.
-  iIntros (HΦ) "HP". iApply wp_bin_op_pure. by intros; do 2 constructor.
-  rewrite HΦ. iNext. iIntros (?? Heval). by inversion_clear Heval; inv_lit.
+  iIntros (HΦ) "HP". iApply wp_bin_op_pure; try done.
+  - by intros; do 2 constructor.
+  - rewrite HΦ. iNext. iIntros (?? Heval). by inversion_clear Heval; inv_lit.
 Qed.
 
 Lemma wp_offset E l z Φ :
   ▷ Φ (LitV $ LitLoc $ l +ₗ z) -∗
     WP BinOp OffsetOp (Lit $ LitLoc l) (Lit $ LitInt z) @ E {{ Φ }}.
 Proof.
-  iIntros "HP". iApply wp_bin_op_pure; first by econstructor.
+  iIntros "HP". iApply wp_bin_op_pure; first (by econstructor); first done.
   iNext. iIntros (?? Heval). inversion_clear Heval. done.
 Qed.
 
@@ -344,7 +346,7 @@ Lemma wp_plus E z1 z2 Φ :
   ▷ Φ (LitV $ LitInt $ z1 + z2) -∗
     WP BinOp PlusOp (Lit $ LitInt z1) (Lit $ LitInt z2) @ E {{ Φ }}.
 Proof.
-  iIntros "HP". iApply wp_bin_op_pure; first by econstructor.
+  iIntros "HP". iApply wp_bin_op_pure; first (by econstructor); first done.
   iNext. iIntros (?? Heval). inversion_clear Heval. done.
 Qed.
 
@@ -352,7 +354,7 @@ Lemma wp_minus E z1 z2 Φ :
   ▷ Φ (LitV $ LitInt $ z1 - z2) -∗
     WP BinOp MinusOp (Lit $ LitInt z1) (Lit $ LitInt z2) @ E {{ Φ }}.
 Proof.
-  iIntros "HP". iApply wp_bin_op_pure; first by econstructor.
+  iIntros "HP". iApply (wp_bin_op_pure with "[//]"); first by econstructor.
   iNext. iIntros (?? Heval). inversion_clear Heval. done.
 Qed.
 
@@ -381,7 +383,7 @@ Lemma wp_app_ind E f (el : list expr) (Ql : vec (val → iProp Σ) (length el))
 Proof.
   intros [vf Hf]. revert vs Ql.
   induction el as [|e el IH]=>/= vs Ql; inv_vec Ql; simpl.
-  - iIntros "H". iSpecialize ("H" $! [#]). rewrite !app_nil_r /=. by iApply "H".
+  - iIntros "_ H". iSpecialize ("H" $! [#]). rewrite !app_nil_r /=. by iApply "H".
   - iIntros (Q Ql) "[He Hl] HΦ".
     assert (App f ((of_val <$> vs) ++ e :: el) = fill_item (AppRCtx vf vs el) e)
       as -> by rewrite /= (of_to_val f) //.
diff --git a/theories/lang/proofmode.v b/theories/lang/proofmode.v
index 6ed7298bad4ccf3d97298e9569a4de78b6a8fd25..d817658df83c25ee54578502e69905e1606e88fb 100644
--- a/theories/lang/proofmode.v
+++ b/theories/lang/proofmode.v
@@ -26,7 +26,7 @@ Ltac wp_done :=
   | _ => fast_done
   end.
 
-Ltac wp_value_head := etrans; [|eapply wp_value; wp_done]; lazy beta.
+Ltac wp_value_head := etrans; [|eapply wp_value; apply _]; simpl.
 
 Ltac wp_seq_head :=
   lazymatch goal with
diff --git a/theories/lang/tactics.v b/theories/lang/tactics.v
index 58955702511792aa470d5930ab1328c86eb0ce68..11efdd22f157a236e15fe732e2083350baa18739 100644
--- a/theories/lang/tactics.v
+++ b/theories/lang/tactics.v
@@ -174,6 +174,7 @@ Ltac solve_closed :=
 Hint Extern 0 (Closed _ _) => solve_closed : typeclass_instances.
 
 Ltac solve_to_val :=
+  rewrite /IntoVal;
   try match goal with
   | |- context E [language.to_val ?e] =>
      let X := context E [to_val e] in change X
@@ -186,6 +187,7 @@ Ltac solve_to_val :=
      let e' := W.of_expr e in change (is_Some (to_val (W.to_expr e')));
      apply W.to_val_is_Some, (bool_decide_unpack _); vm_compute; exact I
   end.
+Hint Extern 10 (IntoVal _ _) => solve_to_val : typeclass_instances.
 
 Ltac solve_atomic :=
   match goal with
diff --git a/theories/typing/bool.v b/theories/typing/bool.v
index 84dba1c6bd3053ef11bac5087a46b1335bdd3126..2da29d43c387268357aacb02b2689a12031f2056 100644
--- a/theories/typing/bool.v
+++ b/theories/typing/bool.v
@@ -28,7 +28,7 @@ Section typing.
   Lemma type_bool_instr (b : Datatypes.bool) : typed_val #b bool.
   Proof.
     iIntros (E L tid) "_ _ $ $ _". wp_value.
-    rewrite tctx_interp_singleton tctx_hasty_val. by destruct b.
+    rewrite tctx_interp_singleton tctx_hasty_val' //. by destruct b.
   Qed.
 
   Lemma type_bool (b : Datatypes.bool) E L C T x e :
diff --git a/theories/typing/function.v b/theories/typing/function.v
index 5bf2834649e50884b76e31939835bd1217648ab7..044c40b94f3f4bd8a8430f732bd5eea1e83ff26b 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -21,7 +21,7 @@ Section fn.
      That would be slightly simpler, but, unfortunately, we are no longer
      able to prove that this is contractive. *)
   Program Definition fn (fp : A → fn_params) : type :=
-    {| st_own tid vl := (∃ fb kb xb e H,
+    {| st_own tid vl := tc_opaque (∃ fb kb xb e H,
          ⌜vl = [@RecV fb (kb::xb) e H]⌝ ∗ ⌜length xb = n⌝ ∗
          ▷ ∀ (x : A) (ϝ : lft) (k : val) (xl : vec val (length xb)),
             □ typed_body ((fp x).(fp_E)  ϝ) [ϝ ⊑ₗ []]
@@ -32,6 +32,9 @@ Section fn.
   Next Obligation.
     iIntros (fp tid vl) "H". iDestruct "H" as (fb kb xb e ?) "[% _]". by subst.
   Qed.
+  Next Obligation.
+    unfold tc_opaque. apply _.
+  Qed.
 
   (* FIXME : This definition is less restrictive than the one used in
      Rust. In Rust, the type of parameters are taken into account for
@@ -259,7 +262,7 @@ Section typing.
                vmap (λ ty (v : val), tctx_elt_interp tid (v ◁ box ty)) (fp x).(fp_tys))%I
             with "[Hargs]"); first wp_done.
     - rewrite /=. iSplitR "Hargs".
-      { simpl. iApply wp_value; last done. solve_to_val. }
+      { simpl. iApply wp_value. by unlock. }
       remember (fp_tys (fp x)) as tys. clear dependent k' p HE fp x.
       iInduction ps as [|p ps] "IH" forall (tys); first by simpl.
       simpl in tys. inv_vec tys=>ty tys. simpl.
@@ -410,7 +413,7 @@ Section typing.
     typed_instruction_ty E L T ef (fn fp).
   Proof.
     iIntros (-> -> Hc) "#Hbody". iIntros (tid) "#LFT _ $ $ #HT". iApply wp_value.
-    { simpl. rewrite ->(decide_left Hc). done. }
+    { unfold IntoVal. 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.
diff --git a/theories/typing/int.v b/theories/typing/int.v
index ed6a41ae4242319046e5352499099c5cbc8678ba..9643e8ba81e78888791bad5c6d35d251cd6ab458 100644
--- a/theories/typing/int.v
+++ b/theories/typing/int.v
@@ -27,7 +27,7 @@ Section typing.
   Lemma type_int_instr (z : Z) : typed_val #z int.
   Proof.
     iIntros (E L tid) "_ _ $ $ _". wp_value.
-    by rewrite tctx_interp_singleton tctx_hasty_val.
+    by rewrite tctx_interp_singleton tctx_hasty_val' //.
   Qed.
 
   Lemma type_int (z : Z) E L C T x e :
diff --git a/theories/typing/lib/rc/rc.v b/theories/typing/lib/rc/rc.v
index 4835e61ec5f6037e1bc4b8abf51fe5ea2efa1c82..dbc6ede2ba4b896f4a9a6f4b8638e839a8416ff5 100644
--- a/theories/typing/lib/rc/rc.v
+++ b/theories/typing/lib/rc/rc.v
@@ -80,7 +80,7 @@ Section rc.
   Qed.
 
   Definition rc_persist tid ν (γ : gname) (l : loc) (ty : type) : iProp Σ :=
-    (∃ ty', ▷ type_incl ty' ty ∗
+    tc_opaque (∃ ty', ▷ type_incl ty' ty ∗
               na_inv tid rc_invN (rc_inv tid ν γ l ty') ∗
               (* We use this disjunction, and not simply [ty_shr] here,
                  because [weak_new] cannot prove ty_shr, even for a dead
@@ -88,6 +88,9 @@ Section rc.
               (ty.(ty_shr) ν tid (l +ₗ 2) ∨ [†ν]) ∗
               □ (1.[ν] ={↑lftN,∅}▷=∗ [†ν]))%I.
 
+  Global Instance rc_persist_persistent : PersistentP (rc_persist tid ν γ l ty).
+  Proof. unfold rc_persist, tc_opaque. apply _. Qed.
+
   Global Instance rc_persist_ne ν γ l n :
     Proper (type_dist2 n ==> dist n) (rc_persist tid ν γ l).
   Proof.
@@ -166,7 +169,9 @@ Section rc.
         iExists _, _, _. iFrame. iExists ty. iFrame "#". iSplitR; last by auto.
           by iApply type_incl_refl. }
       iDestruct "HX" as (γ ν q') "(#Hpersist & Hrctok)".
-      iMod ("Hclose2" with "[] Hrctok") as "[HX $]"; first by (unfold X; auto 10).
+      iMod ("Hclose2" with "[] Hrctok") as "[HX $]".
+      { unfold X. iIntros "!> [??] !>". iNext. iRight. do 3 iExists _.
+        iFrame "#∗". }
       iAssert C with "[>HX]" as "#$".
       { iExists _, _, _. iFrame "Hpersist".
         iMod (bor_sep with "LFT HX") as "[Hrc Hlft]"; first solve_ndisj.
@@ -1027,7 +1032,7 @@ Section code.
         iApply type_jump; solve_typing.
       + wp_op; [lia|move=>_]. wp_if. wp_op. rewrite shift_loc_0. wp_write. wp_op.
         wp_op. wp_write. wp_bind (new _). iSpecialize ("Hrc" with "Hl1 Hl2").
-        iApply (wp_step_fupd with "Hrc"); [done..|]. iApply wp_new; first lia.
+        iApply (wp_step_fupd with "Hrc"); [done..|]. iApply wp_new; first lia. done.
         iNext. iIntros (lr [|? [|??]]) "/= (% & [H†|%] & H↦lr) [Hty Hproto] !>"; try lia.
         rewrite 2!heap_mapsto_vec_cons. iDestruct "H↦lr" as "(Hlr1 & Hlr2 & Hlr3)".
         wp_let. wp_op. rewrite shift_loc_0. wp_write. wp_op. wp_write. wp_op. wp_op.
@@ -1048,7 +1053,7 @@ Section code.
                   tctx_hasty_val' //. unlock. iFrame. }
         iApply type_assign; [solve_typing..|].
         iApply type_jump; solve_typing.
-    - wp_apply wp_new; first lia.
+    - wp_apply wp_new; first lia. done.
       iIntros (lr [|? [|??]]) "/= (% & [H†|%] & H↦lr)"; try lia.
       iDestruct "Hc" as "[[% ?]|[% [Hproto _]]]"; first lia.
       iMod ("Hproto" with "Hl1") as "[Hna Hty]". wp_let. wp_op.
@@ -1058,7 +1063,7 @@ Section code.
       { iDestruct "Hty" as "[(Hl1 & Hl2 & Hl† & Hl3)|Hty]"; last done.
         iMod (own_alloc (● (Some $ Cinl ((1/2)%Qp, 1%positive), 0%nat) ⋅
                          rc_tok (1/2)%Qp)) as (γ) "[Ha Hf]"=>//.
-        iMod (lft_create with "LFT") as (ν) "[[Hν1 Hν2] Hν†]"=>//.
+        iMod (lft_create with "LFT") as (ν) "[[Hν1 Hν2] #Hν†]"=>//.
         iApply (fupd_mask_mono (↑lftN))=>//. iExists γ, ν, (1/2)%Qp. iFrame.
         iMod (bor_create _ ν with "LFT Hl3") as "[Hb Hh]"=>//. iExists _.
         iSplitR; first by iApply type_incl_refl.
@@ -1104,7 +1109,7 @@ Section code.
               with "[] LFT HE Hna HL Hk [-]"); last first.
       { rewrite 3!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val
                 !tctx_hasty_val' //. unlock. iFrame. iRight. iExists γ, ν, _.
-        iFrame "∗#". auto. }
+        unfold rc_persist, tc_opaque. iFrame "∗#". eauto. }
       iApply type_letalloc_1; [solve_typing..|]. iIntros (rcold). simpl_subst.
       iApply type_let. apply rc_drop_type. solve_typing. iIntros (drop). simpl_subst.
       iApply (type_letcall ()); [solve_typing..|]. iIntros (content). simpl_subst.
diff --git a/theories/typing/lib/refcell/ref_code.v b/theories/typing/lib/refcell/ref_code.v
index ca36f8eab0d6cc56facec2e26310d295347f41d1..7b3e4d5d17644608d1b016d66dcd36c186936715 100644
--- a/theories/typing/lib/refcell/ref_code.v
+++ b/theories/typing/lib/refcell/ref_code.v
@@ -230,7 +230,7 @@ Section ref_functions.
     rewrite {1}heap_mapsto_vec_cons heap_mapsto_vec_singleton.
     iDestruct "Href" as "[[Href↦1 Href↦2] Href]".
     iDestruct "Href" as (ν qν γ β ty') "(#Hshr & #Hαβ & #Hinv & >Hν & Hγ)".
-    wp_read. wp_let. wp_apply wp_new; first done.
+    wp_read. wp_let. wp_apply wp_new; try done.
     iIntros (lx [|? []]) "(% & H† & Hlx)"; try (simpl in *; lia).
     rewrite heap_mapsto_vec_singleton. wp_let. wp_write. wp_let. rewrite tctx_hasty_val.
     iMod (lctx_lft_alive_tok α with "HE HL") as (?) "(Hα & HL & Hclose1)";[solve_typing..|].
diff --git a/theories/typing/lib/refcell/refmut_code.v b/theories/typing/lib/refcell/refmut_code.v
index 396713e73cbecbd762d25fea91f0dd33defd48b6..0e270dd3317cfc30d0a169838faa381089fdb036 100644
--- a/theories/typing/lib/refcell/refmut_code.v
+++ b/theories/typing/lib/refcell/refmut_code.v
@@ -176,7 +176,7 @@ Section refmut_functions.
     rewrite {1}heap_mapsto_vec_cons heap_mapsto_vec_singleton.
     iDestruct "Href" as "[[Href↦1 Href↦2] Href]".
     iDestruct "Href" as (ν γ β ty') "(Hbor & #Hαβ & #Hinv & >Hν & Hγ)".
-    wp_read. wp_let. wp_apply wp_new; first done.
+    wp_read. wp_let. wp_apply wp_new; first done. done.
     iIntros (lx [|? []]) "(% & H† & Hlx)"; try (simpl in *; lia).
     rewrite heap_mapsto_vec_singleton. wp_let. wp_write. wp_let. rewrite tctx_hasty_val.
     iMod (lctx_lft_alive_tok α with "HE HL") as (?) "(Hα & HL & Hclose1)";[solve_typing..|].
diff --git a/theories/typing/own.v b/theories/typing/own.v
index d1b7551dfdab0a973f5d5343cb9f11a5de508aef..9d6b85b411d2794bd06e15ec00924d64b3bded09 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -251,7 +251,7 @@ Section typing.
     typed_instruction_ty E L [] (new [ #n ]%E) (own_ptr n' (uninit n')).
   Proof.
     iIntros (? tid) "#LFT #HE $ $ _".
-    iApply wp_new; first done. iModIntro.
+    iApply wp_new; try done. iModIntro.
     iIntros (l vl) "(% & H† & Hlft)". subst. rewrite tctx_interp_singleton tctx_hasty_val.
     iNext. rewrite freeable_sz_full Z2Nat.id //. iFrame.
     iExists vl. iFrame. by rewrite Nat2Z.id.
@@ -362,7 +362,7 @@ End typing.
 
 Hint Resolve own_mono' own_proper' box_mono' box_proper'
              write_own read_own_copy : lrust_typing.
-(* By setting the priority high, we make sure copying is tryed before
+(* By setting the priority high, we make sure copying is tried before
    moving. *)
 Hint Resolve read_own_move | 100 : lrust_typing.
 
diff --git a/theories/typing/soundness.v b/theories/typing/soundness.v
index 88a0a46a2964e219831d8f36e54099fbf67b80cd..4da62c201f87203fac7ece7397944f3b397733c9 100644
--- a/theories/typing/soundness.v
+++ b/theories/typing/soundness.v
@@ -35,8 +35,8 @@ Section type_soundness.
     cut (adequate (main [exit_cont]%E) ∅ (λ _, True)).
     { split. by eapply adequate_nonracing.
       intros. by eapply (adequate_safe (main [exit_cont]%E)). }
-    apply: lrust_adequacy=>?.
-    iMod lft_init as (?) "#LFT". done.
+    apply: lrust_adequacy=>?. iIntros "_".
+    iMod (lft_init with "[//]") as (?) "#LFT". done.
     iMod na_alloc as (tid) "Htl". set (Htype := TypeG _ _ _ _ _).
     wp_bind (of_val main). iApply (wp_wand with "[Htl]").
     iApply (Hmain _ [] [] $! tid with "LFT [] Htl [] []").
diff --git a/theories/typing/type_context.v b/theories/typing/type_context.v
index aec79f460df6a8511cd8e2d623a1dafdc2e0886d..6e5ec879100b2d6da5ccc394d96333639b16df8d 100644
--- a/theories/typing/type_context.v
+++ b/theories/typing/type_context.v
@@ -40,7 +40,7 @@ Section type_context.
     eval_path p = Some v → (WP p @ E {{ v', ⌜v' = v⌝ }})%I.
   Proof.
     revert v; induction p; intros v; cbn -[to_val];
-      try (intros ?; by iApply wp_value); [].
+      try (simpl; intros ?; simplify_eq; by iApply wp_value); [].
     destruct op; try discriminate; [].
     destruct p2; try (intros ?; by iApply wp_value); [].
     destruct l; try (intros ?; by iApply wp_value); [].