diff --git a/theories/lang/lang.v b/theories/lang/lang.v
index d4f4241087e04e08f476d3c767eacab40dc2bf7e..43acbcd0d061d127f6e74fdbe7529228c451cf0c 100644
--- a/theories/lang/lang.v
+++ b/theories/lang/lang.v
@@ -161,7 +161,8 @@ Arguments subst_v _%binder _ _%E.
 Lemma subst_v_eq (xl : list binder) (vsl : vec val (length xl)) e :
   Some $ subst_v xl vsl e = subst_l xl (of_val <$> vec_to_list vsl) e.
 Proof.
-  revert vsl. induction xl=>/= vsl; inv_vec vsl=>//=v vsl. by rewrite -IHxl.
+  revert vsl. induction xl as [|x xl IHxl]=>/= vsl; inv_vec vsl=>//=v vsl.
+  by rewrite -IHxl.
 Qed.
 
 (** The stepping relation *)
@@ -372,7 +373,8 @@ Lemma list_expr_val_eq_inv vl1 vl2 e1 e2 el1 el2 :
   map of_val vl1 ++ e1 :: el1 = map of_val vl2 ++ e2 :: el2 →
   vl1 = vl2 ∧ el1 = el2.
 Proof.
-  revert vl2; induction vl1; destruct vl2; intros H1 H2; inversion 1.
+  revert vl2; induction vl1 as [|? vl1 IHvl1];
+    intros vl2; destruct vl2 as [|? vl2]; intros H1 H2; inversion 1.
   - done.
   - subst. by rewrite to_of_val in H1.
   - subst. by rewrite to_of_val in H2.
@@ -469,11 +471,13 @@ Qed.
 (** Closed expressions *)
 Lemma is_closed_weaken X Y e : is_closed X e → X ⊆ Y → is_closed Y e.
 Proof.
-  revert e X Y. fix FIX 1; destruct e=>X Y/=; try naive_solver.
+  revert e X Y. fix FIX 1; intros e; destruct e=>X Y/=; try naive_solver.
   - naive_solver set_solver.
   - rewrite !andb_True. intros [He Hel] HXY. split. by eauto.
+    rename select (list expr) into el.
     induction el=>/=; naive_solver.
   - rewrite !andb_True. intros [He Hel] HXY. split. by eauto.
+    rename select (list expr) into el.
     induction el=>/=; naive_solver.
 Qed.
 
@@ -482,12 +486,16 @@ Proof. intros. by apply is_closed_weaken with [], list_subseteq_nil. Qed.
 
 Lemma is_closed_subst X e x es : is_closed X e → x ∉ X → subst x es e = e.
 Proof.
-  revert e X. fix FIX 1; destruct e=> X /=; rewrite ?bool_decide_spec ?andb_True=> He ?;
+  revert e X. fix FIX 1; intros e; destruct e=> X /=; rewrite ?bool_decide_spec ?andb_True=> He ?;
     repeat case_bool_decide; simplify_eq/=; f_equal;
     try by intuition eauto with set_solver.
-  - case He=> _. clear He. induction el=>//=. rewrite andb_True=>?.
+  - case He=> _. clear He.
+    rename select (list expr) into el.
+    induction el=>//=. rewrite andb_True=>?.
     f_equal; intuition eauto with set_solver.
-  - case He=> _. clear He. induction el=>//=. rewrite andb_True=>?.
+  - case He=> _. clear He.
+    rename select (list expr) into el.
+    induction el=>//=. rewrite andb_True=>?.
     f_equal; intuition eauto with set_solver.
 Qed.
 
@@ -503,14 +511,18 @@ Proof. intros <-%of_to_val. apply is_closed_of_val. Qed.
 Lemma subst_is_closed X x es e :
   is_closed X es → is_closed (x::X) e → is_closed X (subst x es e).
 Proof.
-  revert e X. fix FIX 1; destruct e=>X //=; repeat (case_bool_decide=>//=);
+  revert e X. fix FIX 1; intros e; destruct e=>X //=; repeat (case_bool_decide=>//=);
     try naive_solver; rewrite ?andb_True; intros.
   - set_solver.
   - eauto using is_closed_weaken with set_solver.
   - eapply is_closed_weaken; first done.
+    rename select binder into f.
+    rename select (list binder) into xl.
     destruct (decide (BNamed x = f)), (decide (BNamed x ∈ xl)); set_solver.
-  - split; first naive_solver. induction el; naive_solver.
-  - split; first naive_solver. induction el; naive_solver.
+  - split; first naive_solver.
+    rename select (list expr) into el. induction el; naive_solver.
+  - split; first naive_solver.
+    rename select (list expr) into el. induction el; naive_solver.
 Qed.
 
 Lemma subst'_is_closed X b es e :
@@ -571,17 +583,17 @@ Fixpoint expr_beq (e : expr) (e' : expr) : bool :=
   end.
 Lemma expr_beq_correct (e1 e2 : expr) : expr_beq e1 e2 ↔ e1 = e2.
 Proof.
-  revert e1 e2; fix FIX 1.
+  revert e1 e2; fix FIX 1. intros e1 e2.
     destruct e1 as [| | | |? el1| | | | | |? el1|],
              e2 as [| | | |? el2| | | | | |? el2|]; simpl; try done;
   rewrite ?andb_True ?bool_decide_spec ?FIX;
   try (split; intro; [destruct_and?|split_and?]; congruence).
   - match goal with |- context [?F el1 el2] => assert (F el1 el2 ↔ el1 = el2) end.
-    { revert el2. induction el1 as [|el1h el1q]; destruct el2; try done.
+    { revert el2. induction el1 as [|el1h el1q]; intros el2; destruct el2; try done.
       specialize (FIX el1h). naive_solver. }
     clear FIX. naive_solver.
   - match goal with |- context [?F el1 el2] => assert (F el1 el2 ↔ el1 = el2) end.
-    { revert el2. induction el1 as [|el1h el1q]; destruct el2; try done.
+    { revert el2. induction el1 as [|el1h el1q]; intros el2; destruct el2; try done.
       specialize (FIX el1h). naive_solver. }
     clear FIX. naive_solver.
 Qed.
diff --git a/theories/lang/races.v b/theories/lang/races.v
index 9c923d16b3bb559d6299e631353459b23824f250..cb06828d42bd25d4c7da7acf0b8949f5cbaf3a1f 100644
--- a/theories/lang/races.v
+++ b/theories/lang/races.v
@@ -30,24 +30,24 @@ Inductive next_access_head : expr → state → access_kind * order → loc →
 Goal ∀ e1 e2 e3 σ, head_reducible (CAS e1 e2 e3) σ →
                    ∃ a l, next_access_head (CAS e1 e2 e3) σ a l.
 Proof.
-  intros ??? σ (?&?&?&?&?). inversion H; do 2 eexists;
+  intros ??? σ (?&?&?&?&H). inversion H; do 2 eexists;
     (eapply Access_cas_fail; done) || eapply Access_cas_suc; done.
 Qed.
 Goal ∀ o e σ, head_reducible (Read o e) σ →
               ∃ a l, next_access_head (Read o e) σ a l.
 Proof.
-  intros ?? σ (?&?&?&?&?). inversion H; do 2 eexists; eapply Access_read; done.
+  intros ?? σ (?&?&?&?&H). inversion H; do 2 eexists; eapply Access_read; done.
 Qed.
 Goal ∀ o e1 e2 σ, head_reducible (Write o e1 e2) σ →
               ∃ a l, next_access_head (Write o e1 e2) σ a l.
 Proof.
-  intros ??? σ (?&?&?&?&?). inversion H; do 2 eexists;
+  intros ??? σ (?&?&?&?&H). inversion H; do 2 eexists;
     eapply Access_write; try done; eexists; done.
 Qed.
 Goal ∀ e1 e2 σ, head_reducible (Free e1 e2) σ →
               ∃ a l, next_access_head (Free e1 e2) σ a l.
 Proof.
-  intros ?? σ (?&?&?&?&?). inversion H; do 2 eexists; eapply Access_free; done.
+  intros ?? σ (?&?&?&?&H). inversion H; do 2 eexists; eapply Access_free; done.
 Qed.
 
 Definition next_access_thread (e: expr) (σ : state)
@@ -93,11 +93,12 @@ Lemma next_access_head_reducible_state e σ a l :
   end.
 Proof.
   intros Ha (κ&e'&σ'&ef&Hstep) Hrednonstuck. destruct Ha; inv_head_step; eauto.
-  - destruct n; first by eexists. exfalso. eapply Hrednonstuck; last done.
+  - rename select nat into n.
+    destruct n; first by eexists. exfalso. eapply Hrednonstuck; last done.
     by eapply CasStuckS.
   - exfalso. eapply Hrednonstuck; last done.
     eapply CasStuckS; done.
-  - match goal with H : ∀ m, _ |- _ => destruct (H i) as [_ [[]?]] end; eauto.
+  - match goal with H : ∀ m, _ |- context[_ +ₗ ?i] => destruct (H i) as [_ [[]?]] end; eauto.
 Qed.
 
 Lemma next_access_head_Na1Ord_step e1 e2 ef σ1 σ2 κ a l :
@@ -119,9 +120,13 @@ Proof.
   (* Oh my. FIXME. *)
   - eapply lit_eq_state; last done.
     setoid_rewrite <-(not_elem_of_dom (D:=gset loc)). rewrite dom_insert_L.
+    rename select loc into l.
+    rename select state into σ.
     cut (is_Some (σ !! l)); last by eexists. rewrite -(elem_of_dom (D:=gset loc)). set_solver+.
   - eapply lit_eq_state; last done.
     setoid_rewrite <-(not_elem_of_dom (D:=gset loc)). rewrite dom_insert_L.
+    rename select loc into l.
+    rename select state into σ.
     cut (is_Some (σ !! l)); last by eexists. rewrite -(elem_of_dom (D:=gset loc)). set_solver+.
 Qed.
 
@@ -191,7 +196,7 @@ Proof.
   { eapply (next_access_head_reductible_ctx e1 σ σ a1 l K1), Hsafe, fill_not_val=>//.
     abstract set_solver. }
   assert (Hnse1:head_reduce_not_to_stuck e1 σ).
-  { eapply safe_not_reduce_to_stuck with (K:=K1); first done. set_solver+. }
+  { eapply (safe_not_reduce_to_stuck _ _ K1); first done. set_solver+. }
   assert (Hσe1:=next_access_head_reducible_state _ _ _ _ Ha1 Hrede1 Hnse1).
   destruct Hrede1 as (κ1'&e1'&σ1'&ef1&Hstep1). clear Hnse1.
   assert (Ha1' : a1.2 = Na1Ord → next_access_head e1' σ1' (a1.1, Na2Ord) l).
@@ -208,14 +213,14 @@ Proof.
            fill_not_val=>//.
     by auto. abstract set_solver. by destruct Hstep1; inversion Ha1. }
   assert (Hnse1: head_reduce_not_to_stuck e1' σ1').
-  { eapply safe_step_not_reduce_to_stuck with (K:=K1); first done; last done. set_solver+. }
+  { eapply (safe_step_not_reduce_to_stuck _ _ K1); first done; last done. set_solver+. }
 
   assert (to_val e2 = None). by destruct Ha2.
   assert (Hrede2:head_reducible e2 σ).
   { eapply (next_access_head_reductible_ctx e2 σ σ a2 l K2), Hsafe, fill_not_val=>//.
     abstract set_solver. }
   assert (Hnse2:head_reduce_not_to_stuck e2 σ).
-  { eapply safe_not_reduce_to_stuck with (K:=K2); first done. set_solver+. }
+  { eapply (safe_not_reduce_to_stuck _ _ K2); first done. set_solver+. }
   assert (Hσe2:=next_access_head_reducible_state _ _ _ _ Ha2 Hrede2 Hnse2).
   destruct Hrede2 as (κ2'&e2'&σ2'&ef2&Hstep2).
   assert (Ha2' : a2.2 = Na1Ord → next_access_head e2' σ2' (a2.1, Na2Ord) l).
@@ -232,7 +237,7 @@ Proof.
            fill_not_val=>//.
     by auto. abstract set_solver. by destruct Hstep2; inversion Ha2. }
   assert (Hnse2':head_reduce_not_to_stuck e2' σ2').
-  { eapply safe_step_not_reduce_to_stuck with (K:=K2); first done; last done. set_solver+. }
+  { eapply (safe_step_not_reduce_to_stuck _ _ K2); first done; last done. set_solver+. }
 
   assert (Ha1'2 : a1.2 = Na1Ord → next_access_head e2 σ1' a2 l).
   { intros HNa. eapply next_access_head_Na1Ord_concurent_step=>//.
@@ -241,7 +246,7 @@ Proof.
   { intros. eapply (next_access_head_reductible_ctx e2 σ1' σ  a2 l K2), Hsafe, fill_not_val=>//.
     abstract set_solver. }
   assert (Hnse1_2:head_reduce_not_to_stuck e2 σ1').
-  { eapply safe_not_reduce_to_stuck with (K:=K2).
+  { eapply (safe_not_reduce_to_stuck _ _ K2).
     - intros. eapply Hsafe. etrans; last done. done. done. done.
     - set_solver+. }
   assert (Hσe1'1:=
@@ -256,7 +261,7 @@ Proof.
   { intros. eapply (next_access_head_reductible_ctx e1 σ2' σ a1 l K1), Hsafe, fill_not_val=>//.
     abstract set_solver. }
   assert (Hnse2_1:head_reduce_not_to_stuck e1 σ2').
-  { eapply safe_not_reduce_to_stuck with (K:=K1).
+  { eapply (safe_not_reduce_to_stuck _ _ K1).
     - intros. eapply Hsafe. etrans; last done. done. done. done.
     - set_solver+. }
   assert (Hσe2'1:=
@@ -283,7 +288,7 @@ Proof.
   destruct Hrede1_2 as (κ2'&e2'&σ'&ef&?).
   inv_head_step.
   match goal with
-  | H : <[l:=_]> σ !! l = _ |- _ => by rewrite lookup_insert in H
+  | H : <[?l:=_]> ?σ !! ?l = _ |- _ => by rewrite lookup_insert in H
   end.
 Qed.
 
diff --git a/theories/lang/tactics.v b/theories/lang/tactics.v
index f20d3db1baf103ebd2a6f6ffd466de206a3b0ac8..27de562405edbad80c0fafa25042c90ee1192846 100644
--- a/theories/lang/tactics.v
+++ b/theories/lang/tactics.v
@@ -87,10 +87,10 @@ Fixpoint is_closed (X : list string) (e : expr) : bool :=
   end.
 Lemma is_closed_correct X e : is_closed X e → lang.is_closed X (to_expr e).
 Proof.
-  revert e X. fix FIX 1; destruct e=>/=;
+  revert e X. fix FIX 1; intros e; destruct e=>/=;
     try naive_solver eauto using is_closed_to_val, is_closed_weaken_nil.
-  - induction el=>/=; naive_solver.
-  - induction el=>/=; naive_solver.
+  - rename select (list expr) into el. induction el=>/=; naive_solver.
+  - rename select (list expr) into el. induction el=>/=; naive_solver.
 Qed.
 
 (* We define [to_val (ClosedExpr _)] to be [None] since [ClosedExpr]
@@ -139,10 +139,10 @@ Fixpoint subst (x : string) (es : expr) (e : expr)  : expr :=
 Lemma to_expr_subst x er e :
   to_expr (subst x er e) = lang.subst x (to_expr er) (to_expr e).
 Proof.
-  revert e x er. fix FIX 1; destruct e=>/= ? er; repeat case_bool_decide;
+  revert e x er. fix FIX 1; intros e; destruct e=>/= ? er; repeat case_bool_decide;
     f_equal; eauto using is_closed_nil_subst, is_closed_to_val, eq_sym.
-  - induction el=>//=. f_equal; auto.
-  - induction el=>//=. f_equal; auto.
+  - rename select (list expr) into el. induction el=>//=. f_equal; auto.
+  - rename select (list expr) into el. induction el=>//=. f_equal; auto.
 Qed.
 
 Definition is_atomic (e: expr) : bool :=
diff --git a/theories/lifetime/model/accessors.v b/theories/lifetime/model/accessors.v
index 58054f9ca77d730af155cc20e72b0dcad64ef015..90b1b968ac5bb2aa0504f0b0b79bb942ef2b3b3e 100644
--- a/theories/lifetime/model/accessors.v
+++ b/theories/lifetime/model/accessors.v
@@ -166,7 +166,7 @@ Proof.
     iMod ("Hclose'" with "[-Hbor Hclose]") as "_".
     { iExists _, _. iFrame. rewrite big_sepS_later. iApply "Hclose''".
       iLeft. iFrame "%". iExists _, _. iFrame. }
-    iExists κ''. iFrame "#". iIntros "!>* HvsQ HQ". clear -HE.
+    iExists κ''. iFrame "#". iIntros "!> %Q HvsQ HQ". clear -HE.
     iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose'".
     iDestruct (own_bor_auth with "HI Hbor") as %Hκ'.
     rewrite big_sepS_later big_sepS_elem_of_acc ?elem_of_dom //
@@ -234,7 +234,7 @@ Proof.
       as %[EQB%to_borUR_included _]%auth_both_valid_discrete.
     iMod (slice_delete_full _ _ true with "Hs Hbox") as (Pb') "(HP' & EQ & Hbox)".
       solve_ndisj. by rewrite lookup_fmap EQB. iDestruct ("HPP'" with "HP'") as "$".
-    iMod fupd_mask_subseteq as "Hclose"; last iIntros "!>* HvsQ HQ". solve_ndisj.
+    iMod fupd_mask_subseteq as "Hclose"; last iIntros "!> %Q HvsQ HQ". solve_ndisj.
     iMod "Hclose" as "_". iDestruct (add_vs with "EQ Hvs [HvsQ]") as "Hvs".
     { iNext. iIntros "HQ H†". iApply "HPP'". iApply ("HvsQ" with "HQ H†"). }
     iMod (slice_insert_full _ _ true with "HQ Hbox") as (j) "(% & #Hs' & Hbox)".