From 3e2074fd534c70a1fea83add58ec9f63fe5bfa18 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@cnrs.fr>
Date: Mon, 31 Mar 2025 16:13:47 +0200
Subject: [PATCH] thou shalt not use generated names.

---
 _CoqProject                                   |   1 +
 theories/lang/lang.v                          |  20 +--
 theories/lang/lib/new_delete.v                |   2 +-
 theories/lang/lifting.v                       |   2 +-
 theories/lang/races.v                         | 119 +++++++++---------
 theories/lang/tactics.v                       |   4 +-
 theories/prophecy/prophecy.v                  |   8 +-
 theories/typing/array.v                       |   2 +-
 theories/typing/array_util.v                  |   2 +-
 theories/typing/borrow.v                      |  42 +++----
 theories/typing/examples/inc_vec.v            |   2 +-
 theories/typing/fixpoint.v                    |   6 +-
 theories/typing/function.v                    |  13 +-
 theories/typing/lib/cell.v                    |   2 +-
 theories/typing/lib/maybe_uninit.v            |   2 +-
 theories/typing/lib/mutex/mutex.v             |   6 +-
 theories/typing/lib/mutex/mutexguard.v        |   2 +-
 theories/typing/lib/slice/iter.v              |  15 ++-
 theories/typing/lib/slice/slice_split.v       |   6 +-
 theories/typing/lib/smallvec/smallvec_index.v |   4 +-
 theories/typing/lib/smallvec/smallvec_pop.v   |   2 +-
 theories/typing/lib/vec/vec_pushpop.v         |   2 +-
 theories/typing/lib/vec_util.v                |   2 +-
 theories/typing/own.v                         |   4 +-
 theories/typing/product_split.v               |   4 +-
 theories/typing/programs.v                    |   2 +-
 theories/typing/sum.v                         |   8 +-
 theories/typing/type.v                        |  18 +--
 theories/typing/uniq_bor.v                    |   4 +-
 theories/util/fancy_lists.v                   |  47 +++----
 theories/util/vector.v                        |  12 +-
 31 files changed, 185 insertions(+), 180 deletions(-)

diff --git a/_CoqProject b/_CoqProject
index 43d3a10e..0c79eb2f 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -4,6 +4,7 @@
 # Cannot use non-canonical projections as it causes massive unification failures
 # (https://github.com/coq/coq/issues/6294).
 -arg -w -arg -redundant-canonical-projection
+-arg -mangle-names -arg _
 
 theories/util/basic.v
 theories/util/vector.v
diff --git a/theories/lang/lang.v b/theories/lang/lang.v
index ff962f36..d6936844 100644
--- a/theories/lang/lang.v
+++ b/theories/lang/lang.v
@@ -163,7 +163,7 @@ 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 IH]=>/= vsl; inv_vec vsl=>//=v vsl. by rewrite -IH.
 Qed.
 
 (** The stepping relation *)
@@ -378,11 +378,11 @@ 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 [|v1 vl1 IH]=>vl2; destruct vl2 as [|v vl2]; intros H1 H2; inversion 1.
   - done.
   - subst. by rewrite to_of_val in H1.
   - subst. by rewrite to_of_val in H2.
-  - destruct (IHvl1 vl2); auto. split; f_equal; auto. by apply (inj of_val).
+  - destruct (IH vl2); auto. split; f_equal; auto. by apply (inj of_val).
 Qed.
 
 Lemma fill_item_no_val_inj Ki1 Ki2 e1 e2 :
@@ -475,7 +475,7 @@ 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=>e; destruct e as [| | | | |e el| | | | | |e el|]=>X Y/=; try naive_solver.
   - naive_solver set_solver.
   - rewrite !andb_True. intros [He Hel] HXY. split. by eauto.
     induction el=>/=; naive_solver.
@@ -488,7 +488,8 @@ 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=>e; destruct e as [| | | | |e el| | | | | |e el|]=> 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=>?.
@@ -509,7 +510,8 @@ 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=>e; destruct e as [| |f xl| | |e el| | | | | |e el|]=>X //=;
+    repeat (case_bool_decide=>//=);
     try naive_solver; rewrite ?andb_True; intros.
   - set_solver.
   - eauto using is_closed_weaken with set_solver.
@@ -578,17 +580,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=>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]=>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]=>el2; destruct el2; try done.
       specialize (FIX el1h). naive_solver. }
     clear FIX. naive_solver.
 Qed.
diff --git a/theories/lang/lib/new_delete.v b/theories/lang/lib/new_delete.v
index 4d4dbd69..f1f942ee 100644
--- a/theories/lang/lib/new_delete.v
+++ b/theories/lang/lib/new_delete.v
@@ -24,7 +24,7 @@ Section specs.
     iIntros (? Φ) "_ HΦ". wp_lam. wp_op; case_bool_decide.
     - wp_if. assert (n = 0) as -> by lia. iApply "HΦ".
       rewrite heap_mapsto_vec_nil. auto.
-    - wp_if. wp_alloc l as "H↦" "H†". lia. iApply "HΦ". subst sz. iFrame.
+    - wp_if. wp_alloc l as "H↦" "H†". lia. iApply "HΦ". subst. iFrame.
   Qed.
 
   Lemma wp_delete vl (n: Z) l E :
diff --git a/theories/lang/lifting.v b/theories/lang/lifting.v
index 6172956a..b758c775 100644
--- a/theories/lang/lifting.v
+++ b/theories/lang/lifting.v
@@ -442,7 +442,7 @@ Proof.
       with (fill_item (AppRCtx vf vs el) e).
     iApply wp_bind. iApply (wp_wand with "He"). iIntros (v) "HQ /=".
     rewrite cons_middle (assoc app) -(fmap_app _ _ [v]).
-    iApply (IH _ _ with "Hl"). iIntros "* Hvl". rewrite -assoc.
+    iApply (IH _ _ with "Hl"). iIntros (vl) "Hvl". rewrite -assoc.
     iApply ("HΦ" $! (v:::vl)). iFrame.
 Qed.
 
diff --git a/theories/lang/races.v b/theories/lang/races.v
index dcdba7f9..009d660a 100644
--- a/theories/lang/races.v
+++ b/theories/lang/races.v
@@ -7,52 +7,52 @@ Inductive access_kind : Type := ReadAcc | WriteAcc | FreeAcc.
 
 (* This is a crucial definition; if we forget to sync it with base_step,
    the results proven here are worthless. *)
-Inductive next_access_head : expr → state → access_kind * order → loc → Prop :=
+Inductive next_access_base : expr → state → access_kind * order → loc → Prop :=
 | Access_read ord l σ :
-    next_access_head (Read ord (Lit $ LitLoc l)) σ (ReadAcc, ord) l
+    next_access_base (Read ord (Lit $ LitLoc l)) σ (ReadAcc, ord) l
 | Access_write ord l e σ :
     is_Some (to_val e) →
-    next_access_head (Write ord (Lit $ LitLoc l) e) σ (WriteAcc, ord) l
+    next_access_base (Write ord (Lit $ LitLoc l) e) σ (WriteAcc, ord) l
 | Access_cas_fail l st e1 lit1 e2 lit2 litl σ :
     to_val e1 = Some (LitV lit1) → to_val e2 = Some (LitV lit2) →
     lit_neq lit1 litl → σ !! l = Some (st, LitV litl) →
-    next_access_head (CAS (Lit $ LitLoc l) e1 e2) σ (ReadAcc, ScOrd) l
+    next_access_base (CAS (Lit $ LitLoc l) e1 e2) σ (ReadAcc, ScOrd) l
 | Access_cas_suc l st e1 lit1 e2 lit2 litl σ :
     to_val e1 = Some (LitV lit1) → to_val e2 = Some (LitV lit2) →
     lit_eq σ lit1 litl → σ !! l = Some (st, LitV litl) →
-    next_access_head (CAS (Lit $ LitLoc l) e1 e2) σ (WriteAcc, ScOrd) l
+    next_access_base (CAS (Lit $ LitLoc l) e1 e2) σ (WriteAcc, ScOrd) l
 | Access_free n l σ i :
     0 ≤ i < n →
-    next_access_head (Free (Lit $ LitInt n) (Lit $ LitLoc l))
+    next_access_base (Free (Lit $ LitInt n) (Lit $ LitLoc l))
                      σ (FreeAcc, Na2Ord) (l +ₗ i).
 
 (* Some sanity checks to make sure the definition above is not entirely insensible. *)
 Goal ∀ e1 e2 e3 σ, base_reducible (CAS e1 e2 e3) σ →
-                   ∃ a l, next_access_head (CAS e1 e2 e3) σ a l.
+                   ∃ a l, next_access_base (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 σ, base_reducible (Read o e) σ →
-              ∃ a l, next_access_head (Read o e) σ a l.
+              ∃ a l, next_access_base (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 σ, base_reducible (Write o e1 e2) σ →
-              ∃ a l, next_access_head (Write o e1 e2) σ a l.
+              ∃ a l, next_access_base (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 σ, base_reducible (Free e1 e2) σ →
-              ∃ a l, next_access_head (Free e1 e2) σ a l.
+              ∃ a l, next_access_base (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)
            (a : access_kind * order) (l : loc) : Prop :=
-  ∃ K e', next_access_head e' σ a l ∧ e = fill K e'.
+  ∃ K e', next_access_base e' σ a l ∧ e = fill K e'.
 
 Definition next_accesses_threadpool (el: list expr) (σ : state)
            (a1 a2 : access_kind * order) (l : loc): Prop :=
@@ -71,19 +71,19 @@ Definition nonracing_threadpool (el : list expr) (σ : state) : Prop :=
              nonracing_accesses a1 a2.
 
 Lemma next_access_base_reducible_ctx e σ σ' a l K :
-  next_access_head e σ' a l → reducible (fill K e) σ → base_reducible e σ.
+  next_access_base e σ' a l → reducible (fill K e) σ → base_reducible e σ.
 Proof.
-  intros Hhead Hred. apply prim_base_reducible.
-  - eapply (reducible_fill_inv (K:=ectx_language.fill K)), Hred. destruct Hhead; eauto.
-  - apply ectxi_language_sub_redexes_are_values. intros [] ? ->; inversion Hhead; eauto.
+  intros Hbase Hred. apply prim_base_reducible.
+  - eapply (reducible_fill_inv (K:=ectx_language.fill K)), Hred. destruct Hbase; eauto.
+  - apply ectxi_language_sub_redexes_are_values. intros [] ? ->; inversion Hbase; eauto.
 Qed.
 
-Definition head_reduce_not_to_stuck (e : expr) (σ : state) :=
+Definition base_reduce_not_to_stuck (e : expr) (σ : state) :=
   ∀ κ e' σ' efs, ectx_language.base_step e σ κ e' σ' efs → e' ≠ App (Lit $ LitInt 0) [].
 
 Lemma next_access_base_reducible_state e σ a l :
-  next_access_head e σ a l → base_reducible e σ →
-  head_reduce_not_to_stuck e σ →
+  next_access_base e σ a l → base_reducible e σ →
+  base_reduce_not_to_stuck e σ →
   match a with
   | (ReadAcc, (ScOrd | Na1Ord)) => ∃ v n, σ !! l = Some (RSt n, v)
   | (ReadAcc, Na2Ord) => ∃ v n, σ !! l = Some (RSt (S n), v)
@@ -93,41 +93,46 @@ Lemma next_access_base_reducible_state e σ a l :
   end.
 Proof.
   intros Ha (κ&e'&σ'&ef&Hstep) Hrednonstuck. destruct Ha; inv_base_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 :
-  next_access_head e1 σ1 (a, Na1Ord) l →
+Lemma next_access_base_Na1Ord_step e1 e2 ef σ1 σ2 κ a l :
+  next_access_base e1 σ1 (a, Na1Ord) l →
   base_step e1 σ1 κ e2 σ2 ef →
-  next_access_head e2 σ2 (a, Na2Ord) l.
+  next_access_base e2 σ2 (a, Na2Ord) l.
 Proof.
   intros Ha Hstep. inversion Ha; subst; clear Ha; inv_base_step; constructor; by rewrite to_of_val.
 Qed.
 
-Lemma next_access_head_Na1Ord_concurent_step e1 e1' e2 e'f σ σ' κ a1 a2 l :
-  next_access_head e1 σ (a1, Na1Ord) l →
+Lemma next_access_base_Na1Ord_concurent_step e1 e1' e2 e'f σ σ' κ a1 a2 l :
+  next_access_base e1 σ (a1, Na1Ord) l →
   base_step e1 σ κ e1' σ' e'f →
-  next_access_head e2 σ a2 l →
-  next_access_head e2 σ' a2 l.
+  next_access_base e2 σ a2 l →
+  next_access_base e2 σ' a2 l.
 Proof.
   intros Ha1 Hstep Ha2. inversion Ha1; subst; clear Ha1; inv_base_step;
   destruct Ha2; simplify_eq; econstructor; eauto; try apply lookup_insert.
   (* Oh my. FIXME. *)
   - eapply lit_eq_state; last done.
-    setoid_rewrite <-(not_elem_of_dom (D:=gset loc)). rewrite dom_insert_L.
-    cut (is_Some (σ !! l)); last by eexists. rewrite -(elem_of_dom (D:=gset loc)). set_solver+.
+    setoid_rewrite <-not_elem_of_dom. rewrite dom_insert_L.
+    rename select loc into l.
+    rename select state into σ.
+    cut (is_Some (σ !! l)); last by eexists. rewrite -elem_of_dom. set_solver+.
   - eapply lit_eq_state; last done.
-    setoid_rewrite <-(not_elem_of_dom (D:=gset loc)). rewrite dom_insert_L.
-    cut (is_Some (σ !! l)); last by eexists. rewrite -(elem_of_dom (D:=gset loc)). set_solver+.
+    setoid_rewrite <-not_elem_of_dom. rewrite dom_insert_L.
+    rename select loc into l.
+    rename select state into σ.
+    cut (is_Some (σ !! l)); last by eexists. rewrite -elem_of_dom. set_solver+.
 Qed.
 
-Lemma next_access_head_Free_concurent_step e1 e1' e2 e'f σ σ' κ o1 a2 l :
-  next_access_head e1 σ (FreeAcc, o1) l → base_step e1 σ κ e1' σ' e'f →
-  next_access_head e2 σ a2 l → base_reducible e2 σ' →
+Lemma next_access_base_Free_concurent_step e1 e1' e2 e'f σ σ' κ o1 a2 l :
+  next_access_base e1 σ (FreeAcc, o1) l → base_step e1 σ κ e1' σ' e'f →
+  next_access_base e2 σ a2 l → base_reducible e2 σ' →
   False.
 Proof.
   intros Ha1 Hstep Ha2 Hred2.
@@ -150,7 +155,7 @@ Qed.
 Lemma safe_step_not_reduce_to_stuck el σ K e e' σ' ef κ :
   (∀ el' σ' e', rtc erased_step (el, σ) (el', σ') →
                 e' ∈ el' → to_val e' = None → reducible e' σ') →
-  fill K e ∈ el → base_step e σ κ e' σ' ef → head_reduce_not_to_stuck e' σ'.
+  fill K e ∈ el → base_step e σ κ e' σ' ef → base_reduce_not_to_stuck e' σ'.
 Proof.
   intros Hsafe Hi Hstep κ1 e1 σ1 ? Hstep1 Hstuck.
   cut (reducible (fill K e1) σ1).
@@ -167,7 +172,7 @@ Qed.
 Lemma safe_not_reduce_to_stuck el σ K e :
   (∀ el' σ' e', rtc erased_step (el, σ) (el', σ') →
                 e' ∈ el' → to_val e' = None → reducible e' σ') →
-  fill K e ∈ el → head_reduce_not_to_stuck e σ.
+  fill K e ∈ el → base_reduce_not_to_stuck e σ.
 Proof.
   intros Hsafe Hi κ e1 σ1 ? Hstep1 Hstuck.
   cut (reducible (fill K e1) σ1).
@@ -190,12 +195,12 @@ Proof.
   assert (Hrede1:base_reducible e1 σ).
   { eapply (next_access_base_reducible_ctx e1 σ σ a1 l K1), Hsafe, fill_not_val=>//.
     abstract set_solver. }
-  assert (Hnse1:head_reduce_not_to_stuck e1 σ).
+  assert (Hnse1:base_reduce_not_to_stuck e1 σ).
   { eapply safe_not_reduce_to_stuck with (K:=K1); first done. set_solver+. }
   assert (Hσe1:=next_access_base_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).
-  { intros. eapply next_access_head_Na1Ord_step, Hstep1.
+  assert (Ha1' : a1.2 = Na1Ord → next_access_base e1' σ1' (a1.1, Na2Ord) l).
+  { intros. eapply next_access_base_Na1Ord_step, Hstep1.
     by destruct a1; simpl in *; subst. }
   assert (Hrtc_step1:
     rtc erased_step (t1 ++ fill K1 e1 :: t2 ++ fill K2 e2 :: t3, σ)
@@ -207,19 +212,19 @@ Proof.
     eapply (next_access_base_reducible_ctx e1' σ1' σ1' (a1, Na2Ord) l K1), Hsafe,
            fill_not_val=>//.
     by auto. abstract set_solver. by destruct Hstep1; inversion Ha1. }
-  assert (Hnse1: head_reduce_not_to_stuck e1' σ1').
+  assert (Hnse1: base_reduce_not_to_stuck e1' σ1').
   { eapply safe_step_not_reduce_to_stuck with (K:=K1); first done; last done. set_solver+. }
 
   assert (to_val e2 = None). by destruct Ha2.
   assert (Hrede2:base_reducible e2 σ).
   { eapply (next_access_base_reducible_ctx e2 σ σ a2 l K2), Hsafe, fill_not_val=>//.
     abstract set_solver. }
-  assert (Hnse2:head_reduce_not_to_stuck e2 σ).
+  assert (Hnse2:base_reduce_not_to_stuck e2 σ).
   { eapply safe_not_reduce_to_stuck with (K:=K2); first done. set_solver+. }
   assert (Hσe2:=next_access_base_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).
-  { intros. eapply next_access_head_Na1Ord_step, Hstep2.
+  assert (Ha2' : a2.2 = Na1Ord → next_access_base e2' σ2' (a2.1, Na2Ord) l).
+  { intros. eapply next_access_base_Na1Ord_step, Hstep2.
     by destruct a2; simpl in *; subst. }
   assert (Hrtc_step2:
     rtc erased_step (t1 ++ fill K1 e1 :: t2 ++ fill K2 e2 :: t3, σ)
@@ -231,16 +236,16 @@ Proof.
     eapply (next_access_base_reducible_ctx e2' σ2' σ2' (a2, Na2Ord) l K2), Hsafe,
            fill_not_val=>//.
     by auto. abstract set_solver. by destruct Hstep2; inversion Ha2. }
-  assert (Hnse2':head_reduce_not_to_stuck e2' σ2').
+  assert (Hnse2':base_reduce_not_to_stuck e2' σ2').
   { eapply safe_step_not_reduce_to_stuck with (K:=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=>//.
+  assert (Ha1'2 : a1.2 = Na1Ord → next_access_base e2 σ1' a2 l).
+  { intros HNa. eapply next_access_base_Na1Ord_concurent_step=>//.
     by rewrite <-HNa, <-surjective_pairing. }
   assert (Hrede1_2: base_reducible e2 σ1').
   { intros. eapply (next_access_base_reducible_ctx e2 σ1' σ  a2 l K2), Hsafe, fill_not_val=>//.
     abstract set_solver. }
-  assert (Hnse1_2:head_reduce_not_to_stuck e2 σ1').
+  assert (Hnse1_2:base_reduce_not_to_stuck e2 σ1').
   { eapply safe_not_reduce_to_stuck with (K:=K2).
     - intros. eapply Hsafe. etrans; last done. done. done. done.
     - set_solver+. }
@@ -249,13 +254,13 @@ Proof.
   assert (Hσe1'2:=
     λ Hord, next_access_base_reducible_state _ _ _ _ (Ha1'2 Hord) Hrede1_2 Hnse1_2).
 
-  assert (Ha2'1 : a2.2 = Na1Ord → next_access_head e1 σ2' a1 l).
-  { intros HNa. eapply next_access_head_Na1Ord_concurent_step=>//.
+  assert (Ha2'1 : a2.2 = Na1Ord → next_access_base e1 σ2' a1 l).
+  { intros HNa. eapply next_access_base_Na1Ord_concurent_step=>//.
     by rewrite <-HNa, <-surjective_pairing. }
   assert (Hrede2_1: base_reducible e1 σ2').
   { intros. eapply (next_access_base_reducible_ctx e1 σ2' σ a1 l K1), Hsafe, fill_not_val=>//.
     abstract set_solver. }
-  assert (Hnse2_1:head_reduce_not_to_stuck e1 σ2').
+  assert (Hnse2_1:base_reduce_not_to_stuck e1 σ2').
   { eapply safe_not_reduce_to_stuck with (K:=K1).
     - intros. eapply Hsafe. etrans; last done. done. done. done.
     - set_solver+. }
@@ -266,10 +271,10 @@ Proof.
 
   assert (a1.1 = FreeAcc → False).
   { destruct a1 as [[]?]; inversion 1.
-    eauto using next_access_head_Free_concurent_step. }
+    eauto using next_access_base_Free_concurent_step. }
   assert (a2.1 = FreeAcc → False).
   { destruct a2 as [[]?]; inversion 1.
-    eauto using next_access_head_Free_concurent_step. }
+    eauto using next_access_base_Free_concurent_step. }
 
   destruct Ha1 as [[]|[]| | |], Ha2 as [[]|[]| | |]=>//=; simpl in *;
     repeat match goal with
@@ -283,7 +288,7 @@ Proof.
   destruct Hrede1_2 as (κ2'&e2'&σ'&ef&?).
   inv_base_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 ecc110cc..c0683767 100644
--- a/theories/lang/tactics.v
+++ b/theories/lang/tactics.v
@@ -90,7 +90,7 @@ 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=>e; destruct e as [| | | | | | |e el| | | | | |e el|]=>/=;
     try naive_solver eauto using is_closed_to_val, is_closed_weaken_nil.
   - induction el=>/=; naive_solver.
   - induction el=>/=; naive_solver.
@@ -143,7 +143,7 @@ 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=>e; destruct e as [| | | | | | |e el| | | | | |e el|]=>/= ? 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.
diff --git a/theories/prophecy/prophecy.v b/theories/prophecy/prophecy.v
index c8d18946..5245e4e1 100644
--- a/theories/prophecy/prophecy.v
+++ b/theories/prophecy/prophecy.v
@@ -366,15 +366,15 @@ Proof.
   have InLNe ζ wπ : .{ζ := wπ} ∈ L → ξ ≠ ζ.
   { move=> /(elem_of_list_fmap_1 pli_pv) ??. by subst. }
   move=> [𝔅i j] ?. rewrite elem_of_cons. case (decide (ξ = PrVar 𝔅i j))=> [Eq|Ne].
-  { dependent destruction Eq.
-    rewrite /S' /add_line discrete_fun_lookup_insert lookup_insert. split.
+  { destruct Eq. rewrite /S' /add_line discrete_fun_lookup_insert lookup_insert. split.
     - move=> /(inj (Some ∘ aitem)) ->. by left.
-    - move=> [Eq'|/InLNe ?]; [|done]. by dependent destruction Eq'. }
+    - move=> [Eq'|/InLNe ?]; [|done]. inversion Eq'.
+      match goal with H: existT _ _ = _ |- _ => apply Eqdep.EqdepTheory.inj_pair2 in H end. by subst. }
   have Eqv : S' 𝔅i !! j ≡ S 𝔅i !! j.
   { rewrite /S' /add_line /discrete_fun_insert.
     case (decide (pv_ty ξ = 𝔅i))=> [?|?]; [|done]. simpl_eq.
     case (decide (i = j))=> [?|?]; [|by rewrite lookup_insert_ne]. by subst. }
-  rewrite Eqv Sim. split; [by right|]. case; [|done]=> Eq. by dependent destruction Eq.
+  rewrite Eqv Sim. split; [by right|]. case; [congruence|done].
 Qed.
 
 (** Manipulating Prophecy Observations *)
diff --git a/theories/typing/array.v b/theories/typing/array.v
index 10ac5e0a..9c287bd5 100644
--- a/theories/typing/array.v
+++ b/theories/typing/array.v
@@ -46,7 +46,7 @@ Section array.
     iIntros "{$ξl}ξl". iMod ("Totys" with "ξl") as "[? $]". iExists _. by iFrame.
   Qed.
   Next Obligation.
-    iIntros "*% LFT In In' tys κ'". rewrite -{2}[vπ]vapply_funsep.
+    iIntros (???? vπ) "*% LFT In In' tys κ'". rewrite -{2}[vπ]vapply_funsep.
     iMod (ty_shr_proph_big_sepL with "LFT In In' tys κ'") as "Upd"; [done|].
     iIntros "!>!>". iApply (step_fupdN_wand with "Upd").
     iIntros ">(%&%&%& ξl & Totys) !>". iExists _, _. iSplit; [done|].
diff --git a/theories/typing/array_util.v b/theories/typing/array_util.v
index deab2948..7aed3482 100644
--- a/theories/typing/array_util.v
+++ b/theories/typing/array_util.v
@@ -29,7 +29,7 @@ Section array_util.
       iDestruct ("IH" with "↦owns") as (?) "(↦s & tys)". iExists (_:::_).
       rewrite heap_mapsto_vec_app. iDestruct (ty_size_eq with "ty") as %->.
       iFrame.
-    - iIntros "(%& ↦s & tys)". iInduction aπl as [|] "IH" forall (l); [done|].
+    - iIntros "(%wll & ↦s & tys)". iInduction aπl as [|] "IH" forall (l); [done|].
       inv_vec wll=>/= ??. rewrite heap_mapsto_vec_app.
       iDestruct "↦s" as "[↦ ↦s]". iDestruct "tys" as "[ty tys]".
       iDestruct (ty_size_eq with "ty") as %->. iSplitL "↦ ty".
diff --git a/theories/typing/borrow.v b/theories/typing/borrow.v
index e03aed58..a0f832d5 100644
--- a/theories/typing/borrow.v
+++ b/theories/typing/borrow.v
@@ -105,10 +105,10 @@ Section borrow.
       (λ post '-[(a, a')], ∀a'': 𝔄, post -[(a, a''); (a'', a')]).
   Proof.
     intros κκ'. split; [intros ??? [[??][]]; by apply forall_proper|].
-    iIntros (??[vπ[]]?) "#LFT #PROPH #UNIQ E L [p _] Obs".
+    iIntros (? tid [vπ[]]?) "#LFT #PROPH #UNIQ E L [p _] Obs".
     have ?: Inhabited 𝔄 := populate (vπ inhabitant).1.
     iDestruct (κκ' with "L E") as "#κ⊑κ'". iFrame "L".
-    iDestruct "p" as ([[]|]??) "[⧖ [#In uniq]]"=>//.
+    iDestruct "p" as ([[|l|]|]??) "[⧖ [#In uniq]]"=>//.
     iDestruct "uniq" as (? ξi [Le Eq]) "[ξVo ξBor]". set ξ := PrVar _ ξi.
     move: Le=> /succ_le[?[->?]].
     iMod (rebor with "LFT κ⊑κ' ξBor") as "[ξBor ToξBor]"; [done|].
@@ -183,7 +183,7 @@ Section borrow.
     iDestruct "uniq" as (? ξi [? Eq]) "[ξVo Bor]". set ξ := PrVar _ ξi.
     iMod (bor_acc_cons with "LFT Bor κ") as "[Body ToBor]"; [done|].
     iDestruct "Body" as (? d'') "(_ & ξPc & ↦own)". rewrite split_mt_ptr.
-    case d'' as [|]; [iDestruct "↦own" as ">[]"|].
+    case d'' as [|d'']; [iDestruct "↦own" as ">[]"|].
     iDestruct "↦own" as (?) "(>↦ & ↦ty & †)". iApply wp_fupd.
     iApply wp_cumulative_time_receipt; [done..|]. wp_read. iIntros "⧗1".
     iDestruct (uniq_agree with "ξVo ξPc") as %[<-->].
@@ -196,18 +196,17 @@ Section borrow.
     iMod ("ToBor" with "[↦ ⧗1 † ToξPc] [↦ty ζPc]") as "[Bor κ]"; last first.
     - iExists -[λ π, ((vπ π).1, π ζ)]. iMod ("ToL" with "κ") as "$".
       rewrite right_id tctx_hasty_val'; [|done]. iModIntro. iSplitR "Obs".
-      + iExists _. iFrame "⧖". iFrame "#". iExists d'', _. iFrame "ζVo Bor".
+      + iFrame "⧖ #". iExists d''. iFrame "ζVo Bor".
         iPureIntro. split; by [lia|].
       + iApply proph_obs_impl; [|done]=> π[<-?]. eapply eq_ind; [done|].
         move: (equal_f Eq π)=>/=. by case (vπ π)=>/= ??->.
-    - iExists _, _. iNext. iFrame "↦ty ζPc".
-      iApply persistent_time_receipt_mono; [|done]. lia.
+    - iFrame "↦ty ζPc". iApply persistent_time_receipt_mono; [|done]. lia.
     - iIntros "!> (%&%& >⧖' & ζPc &?)".
       iMod (cumulative_persistent_time_receipt with "TIME ⧗1 ⧖'") as "⧖'";
         [solve_ndisj|].
       iIntros "!>!>". iDestruct ("ToξPc" with "[ζPc]") as "ξPc".
       { iApply (proph_ctrl_eqz with "PROPH ζPc"). }
-      iExists _, _. iFrame "⧖' ξPc". rewrite split_mt_ptr. iExists _. iFrame.
+      iFrame "⧖' ξPc". rewrite split_mt_ptr. iFrame.
   Qed.
 
   Lemma type_deref_uniq_own {𝔄 𝔅l ℭl 𝔇} κ x p e n (ty: type 𝔄)
@@ -261,7 +260,7 @@ Section borrow.
     iIntros (Hκ tid ? [vπ []]) "/= #LFT #TIME #PROPH #UNIQ #HE $ HL [Hp _] Hproph".
     iMod (Hκ with "HE HL") as (q) "[Htok Hclose]"; first solve_ndisj.
     wp_apply (wp_hasty with "Hp").
-    iIntros ([[]|] [|depth1]) "% #Hdepth1 [#Hκκ' H] //=";
+    iIntros ([[|l|]|] [|depth1]) "% #Hdepth1 [#Hκκ' H] //=";
       iDestruct "H" as (d' ξi) "([% %vπEqξ] & ξVo & Huniq)"; first lia.
     move: vπEqξ. set ξ := PrVar _ ξi=> vπEqξ.
     iAssert (κ ⊑ foldr meet static (ty_lfts ty))%I as "Hκ".
@@ -278,12 +277,10 @@ Section borrow.
       &{κ'}(∃ vπ' d', ⧖(S d') ∗ .PC[ω] vπ' d' ∗ l' ↦∗: ty.(ty_own) vπ' d' tid))%I
       with "[] [Hbor Hl ωVo ξPc]") as "[Hbor Htok]".
     { iIntros "!> H !>!>". iDestruct "H" as (l') "(H↦ & (%&%& ωVo & ξPc & ⧖) & H)".
-      iExists _, (S d'). iFrame "⧖ ξPc". rewrite split_mt_uniq_bor. iFrame "Hκ'".
-      iExists _, d', ωi. iFrame "H↦". rewrite /uniq_body.
+      iFrame "⧖ ξPc". rewrite split_mt_uniq_bor. iFrame "Hκ' H↦". rewrite /uniq_body.
       rewrite (proof_irrel (prval_to_inh _) (prval_to_inh (fst ∘ (fst ∘ vπ)))).
       by iFrame. }
-    { iNext. iExists _. iFrame "Hl Hbor". iExists _, _. iFrame.
-      iApply (persistent_time_receipt_mono); [|done]. lia. }
+    { iFrame. iApply (persistent_time_receipt_mono); [|done]. lia. }
     iClear "Hdepth1 Hdepth2'". clear dependent p depth1 Hκ.
     iMod (bor_exists with "LFT Hbor") as (l') "Hbor"; [done|].
     iMod (bor_sep with "LFT Hbor") as "[H↦ Hbor]"; [done|].
@@ -299,10 +296,10 @@ Section borrow.
     iMod (bor_acc_cons with "LFT Hbor Htok") as "[[VoPc Hown] Hclose']"; [done|].
     iDestruct "VoPc" as (vπ' ?) "(Hvo & Hpc & ?)".
     iMod (bi.later_exist_except_0 with "Hown") as (wπ depth3') "(>#? & Hpcω & Hown)".
-    iMod (uniq_strip_later with "ξVo Hpc") as (?->) "[ξVo ξPc]".
+    iMod (uniq_strip_later with "ξVo Hpc") as (EQ ->) "[ξVo ξPc]".
     have ->: vπ' = fst ∘ (fst ∘ vπ).
     (* TODO: remove usage of fun_ext here.  *)
-    { fun_ext => x /=. move: (equal_f H x) => /= y. by inversion y.  }
+    { fun_ext => x /=. move: (equal_f EQ x) => /= y. by inversion y.  }
     iMod (uniq_strip_later with "Hvo Hpcω") as (<-->) "[ωVo ωPc]".
     iMod (uniq_intro (fst ∘ (fst ∘ vπ)) with "PROPH UNIQ") as (ζi) "[ζVo ζPc]"; [done|].
     set ζ := PrVar _ ζi.
@@ -314,21 +311,18 @@ Section borrow.
     iDestruct ("ToζPc" with "ζ") as "ζPc".
     iDestruct ("ToωPc" with "ω") as "ωPc".
     iMod ("Hclose'" $! (∃vπ' d', ⧖ (S d') ∗ .PC[ζ] vπ' d' ∗
-      l' ↦∗: ty.(ty_own) vπ' d' tid)%I with "[Heqz ωVo ωPc Ht] [Hown ζPc]") as "[? Htok]".
+      l' ↦∗: ty.(ty_own) vπ' d' tid)%I with "[Heqz ωVo ωPc Ht] [$Hown $ζPc //]") as "[? Htok]".
     { iIntros "!> H".
       iMod (bi.later_exist_except_0 with "H") as (? ?) "(>#Hd' & Hpc & Hinner)".
       iMod (uniq_update with "UNIQ ωVo ωPc") as "[ωVo ωPc]"; [solve_ndisj|].
-      iSplitR "Hinner ωPc".
-      - iExists _, d'.
-        iMod (cumulative_persistent_time_receipt with "TIME Ht Hd'") as "$";
-          [solve_ndisj|].
-        iFrame. iApply "Heqz". iDestruct (proph_ctrl_eqz with "PROPH Hpc") as "Eqz".
-        iApply (proph_eqz_constr2 with "Eqz []"). iApply proph_eqz_refl.
-      - iExists _, _. by iFrame. }
-    { iExists _, _. by iFrame. }
+      iSplitR "Hinner ωPc"; [|by iFrame]. iExists _, _.
+      iMod (cumulative_persistent_time_receipt with "TIME Ht Hd'") as "$";
+        [solve_ndisj|].
+      iFrame. iApply "Heqz". iDestruct (proph_ctrl_eqz with "PROPH Hpc") as "Eqz".
+      iApply (proph_eqz_constr2 with "Eqz []"). iApply proph_eqz_refl. }
     iExists -[λ π, ((vπ π).1.1 , π ζ)]. rewrite right_id.
     iMod ("Hclose" with "Htok") as "$". iSplitR "Hproph Hobs".
-    - iExists _, _. iFrame "#". iSplitR; [done|]. iExists _, ζi. by iFrame.
+    - iFrame "#". iExists _. iSplitR; [done|]. by iFrame.
     - iCombine "Hproph Hobs" as "?". iApply proph_obs_impl; [|done]=>/= π.
       move: (equal_f vπEqξ π) (equal_f ωEq π)=>/=. case (vπ π)=> [[??][??]]/=.
       case (π ξ)=> ??[=<-<-<-][Imp[=<-?]]. by apply Imp.
diff --git a/theories/typing/examples/inc_vec.v b/theories/typing/examples/inc_vec.v
index 3fb3fb67..991908a7 100644
--- a/theories/typing/examples/inc_vec.v
+++ b/theories/typing/examples/inc_vec.v
@@ -51,7 +51,7 @@ Section code.
       - intro_subst.
         iApply (type_jump (λ _, +[iter ◁ box (uniq_slice _ int)]));
           [solve_typing|solve_extract|solve_typing|..].
-      - iModIntro. iIntros (? ?). inv_vec vl. simpl_subst. via_tr_impl.
+      - iModIntro. iIntros (? vl). inv_vec vl. simpl_subst. via_tr_impl.
         { iApply type_val; [apply iter_uniq_next_type|]. intro_subst.
           iApply type_newlft. iIntros (γ).
           iApply (type_letalloc_1 (&uniq{γ} _)); [solve_extract| solve_typing |..].
diff --git a/theories/typing/fixpoint.v b/theories/typing/fixpoint.v
index 9e7eb51a..b4c98851 100644
--- a/theories/typing/fixpoint.v
+++ b/theories/typing/fixpoint.v
@@ -54,7 +54,7 @@ Section S.
       + apply (Tn_ty_E_const i 0).
       + done.
       + intros. apply dist_later_0.
-    - case i as [|]; [lia|]. case (IH i) as [??]; [lia|]. split.
+    - case i as [|i]; [lia|]. case (IH i) as [??]; [lia|]. split.
       + intros. apply dist_later_S. apply HT; try done.
         * apply type_contractive_ty_size.
         * apply (Tn_ty_lft_const (2 + i) (2 + n)).
@@ -164,7 +164,7 @@ Section fix_ty.
       (T (fix_ty T)).(ty_own) vπ d tid vl.
     { move=> *. apply equiv_dist=> n. etrans; [apply dist_S, conv_compl|].
       rewrite/= (EqOwn n). symmetry. apply HT=>// *; [apply lft_equiv_refl| |].
-      - destruct n; [by apply dist_later_0|]. apply dist_later_S.
+      - destruct n as [|n]; [by apply dist_later_0|]. apply dist_later_S.
         case (fix_ty_Tn'_dist T (S n))=> [_ _ _ Eq _]. apply dist_S, Eq.
       - case (fix_ty_Tn'_dist T n)=> [_ _ _ _ Eq]. apply Eq. }
     have EqShr': ∀vπ d κ tid l, (fix_ty T).(ty_shr) vπ d κ tid l ≡
@@ -173,7 +173,7 @@ Section fix_ty.
       rewrite/= (EqShr n). symmetry. apply HT=>// *; [apply lft_equiv_refl| |].
       - move: n=> [|[|n]]; [done|done|].
         case (fix_ty_Tn'_dist T (S n))=> [_ _ _ Eq _]. apply dist_S, Eq.
-      - destruct n; [by apply dist_later_0|]. apply dist_later_S.
+      - destruct n as [|n]; [by apply dist_later_0|]. apply dist_later_S.
         case (fix_ty_Tn'_dist T n)=> [_ _ _ _ Eq]. apply Eq. }
     apply eqtype_id_unfold. iIntros "*_!>_". iSplit; [iPureIntro; by apply HT|].
     iSplit; [|iSplit; iIntros "!> *"].
diff --git a/theories/typing/function.v b/theories/typing/function.v
index 8d2ba1d1..cbf3f54c 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -14,7 +14,7 @@ Fixpoint subst_plv {𝔄l} (bl: plistc binder 𝔄l) (vl: plistc val 𝔄l) (e:
 Global Instance do_subst_plv {𝔄l} (bl vl: plistc _ 𝔄l) e :
   DoSubstL bl (map of_val vl) e (subst_plv bl vl e).
 Proof.
-  rewrite /DoSubstL. induction 𝔄l, bl, vl; [done|]=>/=. by rewrite IH𝔄l.
+  rewrite /DoSubstL. induction 𝔄l as [|𝔄 𝔄l IH], bl, vl; [done|]=>/=. by rewrite IH.
 Qed.
 
 Lemma subst_plv_renew {𝔄l 𝔅l} (bl: plistc binder 𝔄l) (vl': plistc val 𝔅l) eq eq' e :
@@ -87,8 +87,8 @@ Section fn.
       case=>/= [??]. rewrite /tctx_elt_interp. do 12 f_equiv. apply Eq.
     - move: (Eq x)=> [_[+ _]]. rewrite {1}/dist.
       move: (fp x).(fp_ityl) (fp' x).(fp_ityl)=> ??. clear=> Eq.
-      induction Eq; [done|]. case wl=> ??. case vπl=> ??/=.
-      f_equiv; [|by apply IHEq]. rewrite /tctx_elt_interp. by do 8 f_equiv.
+      induction Eq as [|t tl x y xl yl Eq Eqs IH]; [done|]. case wl=> ??. case vπl=> ??/=.
+      f_equiv; [|by apply IH]. rewrite /tctx_elt_interp. by do 8 f_equiv.
   Qed.
 End fn.
 
@@ -130,7 +130,7 @@ Section typing.
       - apply (type_lft_morphism_const _ static [])=>//= ?. apply lft_equiv_refl.
       - move=> *. by apply Eq.
       - move=>/= n *. apply bi.exist_ne=> ?. apply bi.sep_ne; [done|].
-        apply uPred_primitive.later_contractive. destruct n; [by apply dist_later_0|].
+        apply uPred_primitive.later_contractive. destruct n as [|n]; [by apply dist_later_0|].
         apply dist_later_S, Eq; try done.
         * intros. destruct n; [by apply dist_later_0|]. by apply dist_later_S.
         * intros. eapply dist_later_dist_lt; [|done]. lia. }
@@ -159,7 +159,8 @@ Section typing.
         by iApply type_lft_morphism_lft_equiv_proper.
     - rewrite !cctx_interp_singleton /cctx_elt_interp. do 3 f_equiv. case=>/= ??.
       do 4 f_equiv. rewrite /tctx_elt_interp. do 6 f_equiv. eapply dist_le; [by apply EqBox|]. lia.
-    - clear -NeITl EqBox Hlt. induction NeITl, wl, aπl; [done|]=>/=.
+    - rename select (_ < n)%nat into Hlt.
+      clear -NeITl EqBox Hlt. induction NeITl, wl, aπl; [done|]=>/=.
       f_equiv; [|done]. rewrite /tctx_elt_interp. do 6 f_equiv. eapply dist_le; [by apply EqBox|]. lia.
   Qed.
 
@@ -281,7 +282,7 @@ Section typing.
       iApply "IH". iModIntro. iApply lft_incl_trans; [done|].
       iApply lft_intersect_incl_r. }
     wp_apply (wp_hasty with "p"). iIntros "*% _". iDestruct 1 as (tr ->?????[=->]) "e".
-    have ->: (λ: ["_r"], Skip;; k' ["_r"])%E = (λ: ["_r"], Skip;; k' ["_r"])%V by unlock.
+    assert ((λ: ["_r"], Skip;; k' ["_r"])%E = (λ: ["_r"], Skip;; k' ["_r"])%V) as ->; [by unlock|].
     iApply (wp_app_hasty_box [] with "ql")=>/=. iIntros (?) "ityl". wp_rec.
     iApply ("e" with "LFT TIME PROPH UNIQ Efp Na [ϝ] [Toκl L k] ityl Obs"); first 2 last.
     { iSplitL; [|done]. iExists _. iSplit; [by rewrite/= left_id|]. by iFrame "ϝ". }
diff --git a/theories/typing/lib/cell.v b/theories/typing/lib/cell.v
index 2e2f36b1..e7b94f6f 100644
--- a/theories/typing/lib/cell.v
+++ b/theories/typing/lib/cell.v
@@ -334,7 +334,7 @@ Section cell.
     eapply type_fn; [apply _|]=> α ??[x[]]. simpl_subst.
     iIntros (?[vπ[]]?) "LFT _ PROPH UNIQ E Na L C /=[x _] Obs".
     rewrite tctx_hasty_val. iDestruct "x" as ([|]) "[_ box]"=>//.
-    case x as [[|x|]|]=>//. iDestruct "box" as "[(%& ↦x & [_ uniq]) †x]".
+    case x as [[|x|]|]=>//. iDestruct "box" as "[(%vl & ↦x & [_ uniq]) †x]".
     wp_apply wp_new; [done..|]. iIntros (?) "[†r ↦r]". wp_seq. case vl as [|[[]|][]]=>//.
     iDestruct "uniq" as (? i [? Eq']) "[Vo Bor]". set ξ := PrVar _ i.
     iMod (lctx_lft_alive_tok α with "E L") as (?) "(α & L & ToL)"; [solve_typing..|].
diff --git a/theories/typing/lib/maybe_uninit.v b/theories/typing/lib/maybe_uninit.v
index d01d6478..329837bd 100644
--- a/theories/typing/lib/maybe_uninit.v
+++ b/theories/typing/lib/maybe_uninit.v
@@ -190,7 +190,7 @@ Section typing.
   Lemma into_maybe_uninit {𝔄} (ty: type 𝔄) E L : subtype E L ty (? ty) Some.
   Proof.
     iIntros "*_!>_". iSplit; [done|]. iSplit; [by iApply lft_incl_refl|].
-    iSplit; iIntros "!>*?/="; iRight; iExists vπ; by iFrame.
+    iSplit; iIntros "!>*?/="; iRight; by iFrame.
   Qed.
 
   Definition maybe_uninit_uninit: val := fn: ["x"] := return: ["x"].
diff --git a/theories/typing/lib/mutex/mutex.v b/theories/typing/lib/mutex/mutex.v
index edf309e3..8ff58fb4 100644
--- a/theories/typing/lib/mutex/mutex.v
+++ b/theories/typing/lib/mutex/mutex.v
@@ -77,8 +77,8 @@ Section mutex.
     iSplit; [|iSplit; [done|]]; by [iApply lft_incl_trans|iApply at_bor_shorten].
   Qed.
   Next Obligation.
-    iIntros "*% #LFT #In Bor κ !>". iApply step_fupdN_full_intro. rewrite split_mt_mutex.
-    iMod (bor_acc_cons with "LFT Bor κ") as "[(%&%& big) ToBor]"; [done|].
+    iIntros (? ty ???? l tid ??) "#LFT #In Bor κ !>". iApply step_fupdN_full_intro. rewrite split_mt_mutex.
+    iMod (bor_acc_cons with "LFT Bor κ") as "[(%Φ &%& big) ToBor]"; [done|].
     iMod (bi.later_exist_except_0 with "big") as (??) "(>->& ↦b & >Obs & >⧖ & ↦ty)".
     iMod ("ToBor" $! ((∃b: bool, l ↦ #b) ∗
       ∃vπ d, ⟨π, Φ (vπ π)⟩ ∗ ⧖(S d) ∗ (l +ₗ 1) ↦∗: ty.(ty_own) vπ d tid)%I
@@ -86,7 +86,7 @@ Section mutex.
     { iIntros "!> big !>!>". iDestruct "big" as "[[% ↦b] (%&%& Obs & ⧖ &%& ↦ &?)]".
       iExists _, _, _, _. iFrame "↦b Obs ⧖". iSplit; [done|]. iExists _. iFrame. }
     { iNext. iSplitL "↦b"; [by iExists _|]. iExists _, _. iFrame. }
-    iMod (bor_sep with "LFT Bor") as "[Borb Borty]"; [done|]. clear b.
+    iMod (bor_sep with "LFT Bor") as "[Borb Borty]"; [done|].
     iMod (bor_acc_cons with "LFT Borb κ") as "[>(%b & ↦b) ToBorb]"; [done|].
     iMod (lock_proto_create with "↦b [Borty]") as "Proto".
     { case b; [done|]. by iExact "Borty". }
diff --git a/theories/typing/lib/mutex/mutexguard.v b/theories/typing/lib/mutex/mutexguard.v
index c7a763f4..c2d5df33 100644
--- a/theories/typing/lib/mutex/mutexguard.v
+++ b/theories/typing/lib/mutex/mutexguard.v
@@ -65,7 +65,7 @@ Section mutexguard.
     iSplit; [|by iApply frac_bor_shorten]. by iApply lft_incl_trans.
   Qed.
   Next Obligation.
-    iIntros (????? d κ') "*% #LFT #In Bor κ' //". rewrite split_mt_mutexguard.
+    iIntros (?? ty ?? d κ') "*% #LFT #In Bor κ' //". rewrite split_mt_mutexguard.
     iMod (bor_sep_persistent with "LFT Bor κ'") as "(>% & Bor & κ')"; [done|].
     do 3 (iMod (bor_exists with "LFT Bor") as (?) "Bor"; [done|]).
     iMod (bor_sep_persistent with "LFT Bor κ'") as "(>-> & Bor & κ')"; [done|].
diff --git a/theories/typing/lib/slice/iter.v b/theories/typing/lib/slice/iter.v
index b032044f..0bd2ee52 100644
--- a/theories/typing/lib/slice/iter.v
+++ b/theories/typing/lib/slice/iter.v
@@ -45,14 +45,13 @@ Section iter.
     iMod (lctx_lft_alive_tok β with "E L") as (?) "(β & L & ToL)"; [solve_typing..|].
     iMod (bor_acc with "LFT Bor β") as "[big ToBor]"; [done|]. wp_let.
     iDestruct "big" as (? d') "(#⧖ & Pc & ↦it)". rewrite split_mt_shr_slice.
-    case d' as [|]=>//=. iDestruct "↦it" as (? len aπl->) "(↦ & ↦' & tys)".
+    case d' as [|]=>//=. iDestruct "↦it" as (l len aπl->) "(↦ & ↦' & tys)".
     rewrite freeable_sz_full -heap_mapsto_vec_singleton.
     wp_apply (wp_delete with "[$↦b $†b]"); [done|]. iIntros "_". wp_seq.
     iDestruct (uniq_agree with "Vo Pc") as %[Eq1 ->]. wp_op. wp_read. wp_let.
-    wp_op. wp_case. case len as [|]=>/=.
+    wp_op. wp_case. case len as [|len]=>/=.
     { iMod ("ToBor" with "[Pc ↦ ↦' tys]") as "[Bor β]".
-      { iNext. iExists _, _. rewrite split_mt_shr_slice. iFrame "⧖ Pc".
-        iExists _, _, _. by iFrame. }
+      { setoid_rewrite split_mt_shr_slice. by iFrame "⧖ ∗". }
       iMod ("ToL" with "β L") as "L".
       iApply (type_type +[#it ◁ &uniq{β} (iter_shr α ty)] -[vπ]
         with "[] LFT TIME PROPH UNIQ E Na L C [-] []").
@@ -112,7 +111,7 @@ Section iter.
     wp_apply (wp_delete with "[$↦b $†b]"); [done|]. iIntros "_". wp_seq.
     iDestruct "big" as (aπζil [->?]) "(↦ & ↦' & uniqs)".
     set aaπl := vmap _ _. iDestruct (uniq_agree with "Vo Pc") as %[Eq1 <-].
-    wp_op. wp_read. wp_let. wp_op. wp_case. case len as [|].
+    wp_op. wp_read. wp_let. wp_op. wp_case. case len as [|len].
     { iMod ("ToBor" with "[Pc ↦ ↦' uniqs]") as "[Bor β]".
       { iNext. iExists _, _. rewrite split_mt_uniq_slice. iFrame "⧖ Pc In".
         iExists _, _, _, _. by iFrame. }
@@ -181,11 +180,11 @@ Section iter.
     iMod (lctx_lft_alive_tok β with "E L") as (?) "(β & L & ToL)"; [solve_typing..|].
     iMod (bor_acc with "LFT Bor β") as "[big ToBor]"; [done|]. wp_let.
     iDestruct "big" as (? d') "(#⧖ & Pc & ↦it)". rewrite split_mt_shr_slice.
-    case d' as [|]=>//=. iDestruct "↦it" as (? len aπl->) "(↦ & ↦' & tys)".
+    case d' as [|]=>//=. iDestruct "↦it" as (l len aπl->) "(↦ & ↦' & tys)".
     rewrite freeable_sz_full -heap_mapsto_vec_singleton.
     wp_apply (wp_delete with "[$↦b $†b]"); [done|]. iIntros "_". wp_seq.
     iDestruct (uniq_agree with "Vo Pc") as %[Eq1 ->]. wp_op. wp_read. wp_let.
-    wp_op. wp_case. case len as [|]=>/=.
+    wp_op. wp_case. case len as [|len]=>/=.
     { iMod ("ToBor" with "[Pc ↦ ↦' tys]") as "[Bor β]".
       { iNext. iExists _, _. rewrite split_mt_shr_slice. iFrame "⧖ Pc".
         iExists _, _, _. by iFrame. }
@@ -252,7 +251,7 @@ Section iter.
     wp_apply (wp_delete with "[$↦b $†b]"); [done|]. iIntros "_". wp_seq.
     iDestruct "big" as (aπζil [->?]) "(↦ & ↦' & uniqs)".
     set aaπl := vmap _ _. iDestruct (uniq_agree with "Vo Pc") as %[Eq1 <-].
-    wp_op. wp_read. wp_let. wp_op. wp_case. case len as [|]=>/=.
+    wp_op. wp_read. wp_let. wp_op. wp_case. case len as [|len]=>/=.
     { iMod ("ToBor" with "[Pc ↦ ↦' uniqs]") as "[Bor β]".
       { iNext. iExists _, _. rewrite split_mt_uniq_slice. iFrame "⧖ Pc In".
         iExists _, _, _, _. by iFrame. }
diff --git a/theories/typing/lib/slice/slice_split.v b/theories/typing/lib/slice/slice_split.v
index 950e97e6..6e03db69 100644
--- a/theories/typing/lib/slice/slice_split.v
+++ b/theories/typing/lib/slice/slice_split.v
@@ -56,7 +56,7 @@ Section slice_split.
       setoid_rewrite shift_loc_assoc_nat. setoid_rewrite <-Nat.mul_add_distr_r. iFrame.
     - iApply proph_obs_impl; [|done]=>/= π [?[/Nat2Z.inj<-[_ +]]].
       rewrite Eqi. clear. move: ifin=> ifin ?. eapply eq_ind; [done|]. clear.
-      induction aπl; inv_fin ifin; [done|]=>/= ifin. by move: (IHaπl ifin)=> [=->->].
+      induction aπl as [|??? IH]; inv_fin ifin; [done|]=>/= ifin. by move: (IH ifin)=> [=->->].
   Qed.
 
   (* Rust's split_at_mut *)
@@ -98,7 +98,7 @@ Section slice_split.
       setoid_rewrite <-Nat.mul_add_distr_r. iFrame.
     - iApply proph_obs_impl; [|done]=>/= π [?[/Nat2Z.inj<-[_ +]]].
       rewrite Eqi. clear. move: ifin=> ifin ?. eapply eq_ind; [done|]. clear.
-      induction aπξil; inv_fin ifin; [done|]=>/= ifin.
-      by move: (IHaπξil ifin)=> [=->->].
+      induction aπξil as [|??? IH]; inv_fin ifin; [done|]=>/= ifin.
+      by move: (IH ifin)=> [=->->].
   Qed.
 End slice_split.
diff --git a/theories/typing/lib/smallvec/smallvec_index.v b/theories/typing/lib/smallvec/smallvec_index.v
index 02199fc1..afb50782 100644
--- a/theories/typing/lib/smallvec/smallvec_index.v
+++ b/theories/typing/lib/smallvec/smallvec_index.v
@@ -34,7 +34,7 @@ Section smallvec_index.
     iDestruct "i" as ([|]) "[_ i]"=>//. case i as [[|i|]|]=>//=.
     wp_apply wp_new; [done..|]. iIntros (?) "[†r ↦r]". wp_let.
     iDestruct "v" as "[(%vl & ↦v & svec) †v]". move: d=> [|d]//=.
-    case vl as [|[[]|][]]=>//. iDestruct "svec" as (?????->) "[Bor tys]".
+    case vl as [|[[]|][]]=>//. iDestruct "svec" as (b ??? aπl ->) "[Bor tys]".
     iDestruct "i" as "[(%& ↦i & (%&->&->)) †i]"=>/=.
     iMod (lctx_lft_alive_tok α with "E L") as (?) "(α & L & ToL)"; [solve_typing..|].
     iMod (frac_bor_acc with "LFT Bor α") as (?) "[>↦ Toα]"; [done|].
@@ -45,7 +45,7 @@ Section smallvec_index.
       do 2 rewrite -heap_mapsto_vec_singleton freeable_sz_full.
       wp_apply (wp_delete with "[$↦v $†v]"); [done|]. iIntros "_". wp_seq.
       wp_apply (wp_delete with "[$↦i $†i]"); [done|]. iIntros "_". do 3 wp_seq.
-      iMod (proph_obs_sat with "PROPH Obs") as %(?& inat &?&->& Lkup &_); [done|].
+      iMod (proph_obs_sat with "PROPH Obs") as %(? & inat &?&->& Lkup &_); [done|].
       move: Lkup. rewrite -vec_to_list_apply -vlookup_lookup'. move=> [In _].
       set ifin := nat_to_fin In. have Eqi: inat = ifin by rewrite fin_to_nat_to_fin.
       rewrite cctx_interp_singleton.
diff --git a/theories/typing/lib/smallvec/smallvec_pop.v b/theories/typing/lib/smallvec/smallvec_pop.v
index f11b86fa..395ce657 100644
--- a/theories/typing/lib/smallvec/smallvec_pop.v
+++ b/theories/typing/lib/smallvec/smallvec_pop.v
@@ -44,7 +44,7 @@ Section smallvec_pop.
     iMod (lctx_lft_alive_tok α with "E L") as (?) "(α & L & ToL)"; [solve_typing..|].
     iMod (bor_acc with "LFT Bor α") as "[(%&%& #⧖ & Pc & big) ToBor]"; [done|].
     wp_seq. iDestruct (uniq_agree with "Vo Pc") as %[<-<-]. rewrite split_mt_smallvec.
-    iDestruct "big" as (?? len ex aπl Eq1) "(↦ & big)".
+    iDestruct "big" as (b ? len ex aπl Eq1) "(↦ & big)".
     rewrite !heap_mapsto_vec_cons !shift_loc_assoc.
     iDestruct "↦" as "(↦₀ & ↦₁ & ↦₂ & ↦₃ &_)". wp_op. wp_read. wp_let.
     wp_apply wp_new; [lia|done|]. iIntros (r) "[†r ↦r]".
diff --git a/theories/typing/lib/vec/vec_pushpop.v b/theories/typing/lib/vec/vec_pushpop.v
index ecacb382..ddf1c8de 100644
--- a/theories/typing/lib/vec/vec_pushpop.v
+++ b/theories/typing/lib/vec/vec_pushpop.v
@@ -94,7 +94,7 @@ Section vec_pushpop.
     rewrite split_mt_vec. case d=>// ?.
     iDestruct "↦vec" as (? len ex aπl Eq1) "(↦ & ↦tys & (%wl &%& ↦ex) & †)".
     rewrite !heap_mapsto_vec_cons shift_loc_assoc. iDestruct "↦" as "(↦₀ & ↦₁ & ↦₂ &_)".
-    wp_op. wp_read. wp_let. wp_op. wp_case. case len as [|].
+    wp_op. wp_read. wp_let. wp_op. wp_case. case len as [|len].
     { iMod ("ToBor" with "[↦₀ ↦₁ ↦₂ ↦tys ↦ex † ⧖ Pc]") as "[Bor β]".
       { iNext. iExists _, _. iFrame "⧖ Pc". rewrite split_mt_vec. iExists _, _, _, _.
         rewrite !heap_mapsto_vec_cons heap_mapsto_vec_nil shift_loc_assoc.
diff --git a/theories/typing/lib/vec_util.v b/theories/typing/lib/vec_util.v
index 690c0c1e..00598c1a 100644
--- a/theories/typing/lib/vec_util.v
+++ b/theories/typing/lib/vec_util.v
@@ -41,7 +41,7 @@ Section vec_util.
       x ↦∗len ty.(ty_size)
     }}}.
   Proof.
-    iIntros (?) "(%&%& ↦ & ↦tys & (%vl & %Lvl & ↦ex) & † & (%& ↦x & ty)) ToΦ".
+    iIntros (?) "(%&%ex& ↦ & ↦tys & (%vl & %Lvl & ↦ex) & † & (%& ↦x & ty)) ToΦ".
     rewrite !heap_mapsto_vec_cons shift_loc_assoc trans_big_sepL_mt_ty_own.
     iDestruct "↦" as "(↦₀ & ↦₁ & ↦₂ &_)". iDestruct "↦tys" as (?) "[↦l tys]".
     iDestruct (ty_size_eq with "ty") as %?.
diff --git a/theories/typing/own.v b/theories/typing/own.v
index e3d23997..664405bb 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -87,7 +87,7 @@ Section own.
     iDestruct (ty_own_proph with "LFT In ty κ") as "Upd"; [done|].
     iApply (step_fupdN_wand with "Upd"). iIntros ">(%ξl & %q &%& ξl & Toty) !>".
     iExists ξl, q. iSplit; [done|]. iIntros "{$† $ξl}ξl".
-    iMod ("Toty" with "ξl") as "[?$]". iExists vl. by iFrame.
+    iMod ("Toty" with "ξl") as "[?$]". by iFrame.
   Qed.
   Next Obligation.
     move=> ?????[|?]*/=; [by iIntros|]. iIntros "#LFT #In #In' [%l[↦ ty]] κ !>!>".
@@ -268,7 +268,7 @@ Section typing.
     typed_instr E L +[p ◁ own_ptr n' ty] (delete [ #n; p])%E (λ _, +[])
       (λ post _, post -[]).
   Proof.
-    iIntros (?->??[?[]]) "_ _ _ _ _ $$ [p _] #Obs". wp_bind p.
+    iIntros (n' ->??[?[]]) "_ _ _ _ _ $$ [p _] #Obs". wp_bind p.
     iApply (wp_hasty with "p"). iIntros (?[|?] _) "? own"; [done|].
     setoid_rewrite by_just_loc_ex. iDestruct "own" as (?[=->]) "[(%& >↦ & ty)?]".
     iDestruct (ty_size_eq with "ty") as "#>%Sz". iApply (wp_delete with "[-]").
diff --git a/theories/typing/product_split.v b/theories/typing/product_split.v
index 81c9dc12..0cb67ffb 100644
--- a/theories/typing/product_split.v
+++ b/theories/typing/product_split.v
@@ -24,7 +24,7 @@ Section product_split.
       (hasty_ptr_offsets p ptr tyl (off + off')).
   Proof.
     apply get_tctx_equiv=> ? vπl. move: p off off'.
-    induction tyl, vπl; [done|]=>/= p ??. f_equiv; [|by rewrite IHtyl Nat.add_assoc].
+    induction tyl as [|t tl ty tyl IH], vπl; [done|]=>/= p ??. f_equiv; [|by rewrite IH Nat.add_assoc].
     apply tctx_elt_interp_hasty_path=>/=. case (eval_path p)=>//.
     (do 2 case=>//)=> ?. by rewrite shift_loc_assoc -Nat2Z.inj_add.
   Qed.
@@ -250,7 +250,7 @@ Section product_split.
       eapply tctx_incl_trans; [by apply tctx_split_uniq_prod|]. apply tctx_incl_tail.
       eapply tctx_incl_trans; [by apply IH|]. eapply proj1, get_tctx_equiv=> ? vπl.
       move: (ty_size _)=> off. rewrite -{2}(Nat.add_0_r off). move: off 0%nat. clear.
-      induction tyl, vπl; [done|]=>/= ??. f_equiv; [|by rewrite IHtyl Nat.add_assoc].
+      induction tyl as [|t tl ty tyl IH], vπl; [done|]=>/= ??. f_equiv; [|by rewrite IH Nat.add_assoc].
       apply tctx_elt_interp_hasty_path=>/=. case (eval_path p)=>//.
       (do 2 case=>//)=> ?. by rewrite shift_loc_assoc Nat2Z.inj_add. }
     by move=>/= ?[[[??][??]][]].
diff --git a/theories/typing/programs.v b/theories/typing/programs.v
index 57a1ec58..9f48a464 100644
--- a/theories/typing/programs.v
+++ b/theories/typing/programs.v
@@ -342,7 +342,7 @@ Section typing.
     case vl as [|v[|]]=>//. rewrite heap_mapsto_vec_singleton. iApply wp_fupd.
     wp_read. iMod ("Toty'" with "↦") as "($&$& ty')". iModIntro.
     iExists -[gt ∘ vπ; st ∘ vπ]. iSplit; [|done]. rewrite right_id
-    tctx_hasty_val tctx_hasty_val'; [|done]. iSplitL "tyb"; iExists d; by iSplit.
+    tctx_hasty_val tctx_hasty_val'; [|done]. iSplitL "tyb"; iExists _; by iSplit.
   Qed.
 
   Lemma type_deref {𝔄 𝔅 𝔄' 𝔄l 𝔅l ℭ} (ty: type 𝔄) (tyb: type 𝔅) (ty': type 𝔄') gt st
diff --git a/theories/typing/sum.v b/theories/typing/sum.v
index b19c6ad7..87e49070 100644
--- a/theories/typing/sum.v
+++ b/theories/typing/sum.v
@@ -38,9 +38,9 @@ Section sum.
   Lemma ty_lfts_lookup_incl {𝔄l} (tyl: typel 𝔄l) i :
     ⊢ tyl_lft tyl ⊑ ty_lft (tyl +!! i).
   Proof.
-    induction tyl; inv_fin i; rewrite /tyl_lft /tyl_lfts /= lft_intersect_list_app;
+    induction tyl as [|ty tyl t tl IH]; inv_fin i; rewrite /tyl_lft /tyl_lfts /= lft_intersect_list_app;
     [by iApply lft_intersect_incl_l|]=> ?.
-    iApply lft_incl_trans; by [iApply lft_intersect_incl_r|iApply IHtyl].
+    iApply lft_incl_trans; by [iApply lft_intersect_incl_r|iApply IH].
   Qed.
 
   Program Definition xsum_ty {𝔄l} (tyl: typel 𝔄l) : type (Σ! 𝔄l) := {|
@@ -126,10 +126,10 @@ Section typing.
           elctx_interp E ∗ elctx_interp ty.(ty_E) ∗ [∗ list] β ∈ βs, β ⊑ ty_lft ty)) ∨
       (∃α E, (∀ty, ⊢ ty_lft (T ty) ≡ₗ α) ∧
         (∀ty, elctx_interp (T ty).(ty_E) ⊣⊢ elctx_interp E)); [|by eleft|by eright].
-    induction All=>/=.
+    induction All as [|???? H ? IH]=>/=.
     { right. exists static, []. split=> ?; by [|apply lft_equiv_refl]. }
     setoid_rewrite lft_intersect_list_app.
-    case IHAll=> [[α[βs[E[Hα HE]]]]|[α[E[Hα HE]]]];
+    case IH=> [[α[βs[E[Hα HE]]]]|[α[E[Hα HE]]]];
     case H=> [α' βs' E' Hα' HE'|α' E' Hα' HE'].
     - left. exists (α' ⊓ α), (βs' ++ βs), (E' ++ E). split=> ?.
       + iApply lft_equiv_trans.
diff --git a/theories/typing/type.v b/theories/typing/type.v
index 1d8e38e1..3fcfc5de 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -242,7 +242,7 @@ Next Obligation. eauto. Qed.
 Next Obligation.
   move=> * /=. iIntros "_ _[%[->?]]". iIntros "$ !>".
   iApply step_fupdN_full_intro. iModIntro. iExists [], 1%Qp.
-  do 2 (iSplit; [done|]). iIntros "_!>". iExists v. by iSplit.
+  do 2 (iSplit; [done|]). iIntros "_!>". iExists _. by iSplit.
 Qed.
 
 Coercion st_of_pt: plain_type >-> simple_type.
@@ -314,12 +314,12 @@ Section ofe_lemmas.
   Global Instance tyl_lfts_ne {𝔄l} n : Proper (dist n ==> (=)) (tyl_lfts (𝔄l:=𝔄l)).
   Proof.
     rewrite /tyl_lfts /dist=> tyl tyl' Eq. f_equal.
-    induction Eq; [done|]. by rewrite/= H IHEq.
+    induction Eq as [|ty tyl x y xl yl Eq Eql IH]; [done|]. by rewrite/= Eq IH.
   Qed.
   Global Instance tyl_lfts_proper {𝔄l} : Proper ((≡) ==> (=)) (tyl_lfts (𝔄l:=𝔄l)).
   Proof.
     rewrite /tyl_lfts /equiv=> tyl tyl' Eq. f_equal.
-    induction Eq; [done|]. by rewrite/= H IHEq.
+    induction Eq as [|ty tyl x y xl yl Eq Eql IH]; [done|]. by rewrite/= Eq IH.
   Qed.
   Global Instance tyl_lft_ne {𝔄l} n : Proper (dist n ==> (=)) (tyl_lft (𝔄l:=𝔄l)).
   Proof. rewrite /tyl_lft. by move=> ??->. Qed.
@@ -328,24 +328,24 @@ Section ofe_lemmas.
   Global Instance tyl_E_ne {𝔄l} n : Proper (dist n ==> (=)) (tyl_E (𝔄l:=𝔄l)).
   Proof.
     rewrite /tyl_E /dist=> tyl tyl' Eq.
-    induction Eq; [done|]. by rewrite/= H IHEq.
+    induction Eq as [|ty tyl x y xl yl Eq Eql IH]; [done|]. by rewrite/= Eq IH.
   Qed.
   Global Instance tyl_E_proper {𝔄l} : Proper ((≡) ==> (=)) (tyl_E (𝔄l:=𝔄l)).
   Proof.
     rewrite /tyl_E /equiv=> tyl tyl' Eq.
-    induction Eq; [done|]. by rewrite/= H IHEq.
+    induction Eq as [|ty tyl x y xl yl Eq Eql IH]; [done|]. by rewrite/= Eq IH.
   Qed.
   Global Instance tyl_outlives_E_ne {𝔄l} n :
     Proper (dist n ==> (=) ==> (=)) (tyl_outlives_E (𝔄l:=𝔄l)).
   Proof.
     rewrite /tyl_outlives_E /dist=> tyl tyl' Eq ??->.
-    induction Eq; [done|]. by rewrite/= H IHEq.
+    induction Eq as [|ty tyl x y xl yl Eq Eql IH]; [done|]. by rewrite/= Eq IH.
   Qed.
   Global Instance tyl_outlives_E_proper {𝔄l} :
     Proper ((≡) ==> (=) ==> (=)) (tyl_outlives_E (𝔄l:=𝔄l)).
   Proof.
     rewrite /tyl_outlives_E /equiv=> tyl tyl' Eq ??->.
-    induction Eq; [done|]. by rewrite/= H IHEq.
+    induction Eq as [|ty tyl x y xl yl Eq Eql IH]; [done|]. by rewrite/= Eq IH.
   Qed.
 
   Global Instance ty_own_ne {𝔄} n:
@@ -620,7 +620,7 @@ Section type_contractive.
       + apply type_lft_morphism_elctx_interp_proper=>//; apply _.
       + intros. destruct n as [|[]]=>//. apply HT'=>// *.
         eapply dist_later_dist_lt; [|done]. lia.
-      + intros. destruct n; [apply dist_later_0|]; apply dist_later_S, HT'=>// *.
+      + intros. destruct n as [|n]; [apply dist_later_0|]; apply dist_later_S, HT'=>// *.
         * destruct n; [apply dist_later_0|]; apply dist_later_S=>//.
         * eapply dist_later_dist_lt; [|done]. lia.
   Qed.
@@ -639,7 +639,7 @@ Section type_contractive.
     - move=> n ????? DIST1 DIST2; apply HT; try (by apply HT').
       + by iApply type_lft_morphism_lft_equiv_proper.
       + apply type_lft_morphism_elctx_interp_proper=>//; apply _.
-      + intros. destruct n; [apply dist_later_0|]. apply dist_later_S, HT'=>// *.
+      + intros. destruct n as [|n]; [apply dist_later_0|]. apply dist_later_S, HT'=>// *.
         * destruct n; [apply dist_later_0|]; apply dist_later_S=>//.
         * eapply dist_later_dist_lt; [|done]. lia.
   Qed.
diff --git a/theories/typing/uniq_bor.v b/theories/typing/uniq_bor.v
index 2465e7dc..78981591 100644
--- a/theories/typing/uniq_bor.v
+++ b/theories/typing/uniq_bor.v
@@ -187,9 +187,9 @@ Section typing.
     Copy ty → lctx_lft_alive E L κ →
     typed_read E L (&uniq{κ} ty) ty (&uniq{κ} ty) fst id.
   Proof.
-    iIntros (? Alv vπ ?[[]|]??) "#LFT E Na L [In uniq] //".
+    iIntros (? Alv vπ d[[]|]??) "#LFT E Na L [In uniq] //".
     have ?: Inhabited 𝔄 := populate (vπ inhabitant).1.
-    iDestruct "uniq" as (??[Le ?]) "[Vo Bor]". case d as [|]; [lia|].
+    iDestruct "uniq" as (?? [Le ?]) "[Vo Bor]". case d as [|]; [lia|].
     iMod (Alv with "E L") as (?) "[κ ToL]"; [done|].
     iMod (bor_acc with "LFT Bor κ") as
       "[(%&%& #>⧖ & Pc &%& >↦ & #ty) ToBor]"; [done|].
diff --git a/theories/util/fancy_lists.v b/theories/util/fancy_lists.v
index 3cb6ad4d..798f1988 100644
--- a/theories/util/fancy_lists.v
+++ b/theories/util/fancy_lists.v
@@ -58,8 +58,8 @@ Fixpoint max_hlist_with {Xl} (f: ∀X, F X → nat) (xl: hlist F Xl) : nat :=
 Lemma max_hlist_with_ge {Xl} (f: ∀X, F X → _) (xl: hlist F Xl) i :
   f _ (hlookup xl i) ≤ max_hlist_with f xl.
 Proof.
-  induction xl; inv_fin i=>/=. { rewrite /llookup /=. lia. }
-  move=> i. etrans; [by apply IHxl|lia].
+  induction xl as [|X Xl x xl IH]; inv_fin i=>/=. { rewrite /llookup /=. lia. }
+  move=> i. etrans; [by apply IH|lia].
 Qed.
 
 Fixpoint happly {Y Xl} (fl: hlist (λ X, Y → F X) Xl) (x: Y)
@@ -89,7 +89,7 @@ Notation "( fl +$.)" := (happly fl) (only parsing).
 Lemma hlookup_apply {A} {F: A → Type} {Xl Y}
     (fl: hlist (λ X, Y → F X) Xl) (x: Y) i :
   (fl +$ x) +!! i = (fl +!! i) x.
-Proof. induction Xl; inv_fin i; inv_hlist fl; [done|]=>/= *. apply IHXl. Qed.
+Proof. induction Xl as [|X Xl IH]; inv_fin i; inv_hlist fl; [done|]=>/= *. apply IH. Qed.
 
 (** * Passive Heterogeneous List *)
 
@@ -240,9 +240,9 @@ Global Instance pbyidx_plookup_iso {A} {F: A → Type} {Xl} :
   Iso (pbyidx (F:=F) (Xl:=Xl)) plookup.
 Proof.
   split; fun_ext.
-  - move=>/= f. fun_ext_dep=> i. induction Xl; inv_fin i; [done|]=>/= ?.
-    by rewrite IHXl.
-  - move=>/= xl. induction Xl; case xl; [done|]=>/= ??. by rewrite IHXl.
+  - move=>/= f. fun_ext_dep=> i. induction Xl as [|X Xl IH]; inv_fin i; [done|]=>/= ?.
+    by rewrite IH.
+  - move=>/= xl. induction Xl as [|X Xl IH]; case xl; [done|]=>/= ??. by rewrite IH.
 Qed.
 
 Lemma pbyidx_plookup {A} {F: A → Type} {Xl} (f: ∀i, F (Xl !!ₗ i)) i :
@@ -324,7 +324,7 @@ Coercion plistc_to_vec: plistc >-> vec.
 
 Lemma plistc_to_vec_lookup {A B} {Xl: list A} (xl: plistc B Xl) i :
   plistc_to_vec xl !!! i = xl -!! i.
-Proof. induction Xl; inv_fin i; case xl; [done|]=>/= _. apply IHXl. Qed.
+Proof. induction Xl as [|X Xl IH]; inv_fin i; case xl; [done|]=>/= _. apply IH. Qed.
 
 Fixpoint plistc_renew {A} {Xl: list A} {A'} {Yl: list A'} {B}
   : eq_nat (length Xl) (length Yl) → plistc B Xl → plistc B Yl :=
@@ -507,31 +507,33 @@ Proof. move=> Imp. elim; constructor; by [apply Imp|]. Qed.
 
 Lemma TCHForall_lookup {Xl} i (Φ: ∀X, F X → Prop) (xl: hlist F Xl) :
   TCHForall Φ xl → Φ _ (xl +!! i).
-Proof. move=> All. induction All; inv_fin i; [done|]. apply IHAll. Qed.
+Proof. move=> All. induction All as [|X Xl x xl Hx ALL IH]; inv_fin i; [done|]. apply IH. Qed.
 
 Lemma HForall_1_lookup {Xl} i (Φ: ∀X, F X → G X → Prop) (xl: _ Xl) yl :
   HForall_1 Φ xl yl → Φ _ (xl +!! i) (yl -!! i).
-Proof. move=> All. induction All; inv_fin i; [done|]. apply IHAll. Qed.
+Proof. move=> All. induction All as [|X Xl x y xl yl Hx ALL IH]; inv_fin i; [done|]. apply IH. Qed.
 
 Lemma HForall_1'_lookup {H: A → A → Type} {Xl Yl} i
     (Φ: ∀X Y, F X → H X Y → Prop) xl (yl: plist2 _ Xl Yl) :
   HForall_1' Φ xl yl → Φ _ _ (xl +!! i) (yl -2!! i).
-Proof. move=> All. induction All; inv_fin i; [done|]. apply IHAll. Qed.
+Proof. move=> All. induction All as [|X Y Xl Yl x y xl yl Hxy ALL IH]; inv_fin i; [done|]. apply IH. Qed.
 
 Lemma HForallTwo_lookup {Xl} i (Φ: ∀X, F X → G X → Prop) (xl: _ Xl) yl :
   HForallTwo Φ xl yl → Φ _ (xl +!! i) (yl +!! i).
-Proof. move=> All. induction All; inv_fin i; [done|]. apply IHAll. Qed.
+Proof. move=> All. induction All as [|X Xl x y xl yl Hxy ALL IH]; inv_fin i; [done|]. apply IH. Qed.
 
 Lemma HForallTwo_forall `{!Inhabited Y} {Xl}
   (Φ: ∀X, Y → F X → G X → Prop) (xl yl: _ Xl) :
   (∀z, HForallTwo (λ X, Φ X z) xl yl) ↔ HForallTwo (λ X x y, ∀z, Φ _ z x y) xl yl.
 Proof.
-  split; [|elim; by constructor]. move=> All. set One := All inhabitant.
-  induction One; [by constructor|]. constructor.
-  { move=> z. move/(.$ z) in All. by dependent destruction All. }
-  have All': ∀z, HForallTwo (λ X, Φ X z) xl yl.
-  { move=> z. move/(.$ z) in All. by dependent destruction All. }
-  auto.
+  split; [|elim; by constructor]. move=> All.
+  induction (All inhabitant) as [|X Xl x y xl yl _ _ IH]; [by constructor|]. constructor.
+  - intros z. specialize (All z). inversion All.
+    repeat match goal with H: existT _ _ = existT _ _ |- _ => apply Eqdep.EqdepTheory.inj_pair2 in H end.
+    by subst.
+  - apply IH. intros z. specialize (All z). inversion All.
+    repeat match goal with H: existT _ _ = existT _ _ |- _ => apply Eqdep.EqdepTheory.inj_pair2 in H end.
+    by subst.
 Qed.
 End Forall.
 
@@ -547,8 +549,9 @@ Proof. move=> >. elim; by constructor. Qed.
 Global Instance HForallTwo_transitive :
   (∀X, Transitive (R X)) → Transitive (HForallTwo R (Xl:=Xl)).
 Proof.
-  move=> ??? zl All. move: zl. elim: All; [done|]=> > ?? IH ? All.
-  dependent destruction All. constructor; by [etrans|apply IH].
+  move=> ??? zl All. move: zl. elim: All; [done|]=> > ?? IH ? All. inversion All.
+  repeat match goal with H: existT _ _ = existT _ _ |- _ => apply Eqdep.EqdepTheory.inj_pair2 in H end.
+  subst. constructor; by [etrans|apply IH].
 Qed.
 
 Global Instance HForallTwo_equivalence :
@@ -661,7 +664,7 @@ Lemma big_sepHL_1_app {F: A → Type} {G Xl Yl}
       (xl: hlist F Xl) (xl': hlist F Yl)
       (yl: plist G Xl) (yl': plist G Yl) (Φ: ∀C, F C → G C → PROP) :
   big_sepHL_1 Φ (xl h++ xl') (yl -++ yl') ⊣⊢ big_sepHL_1 Φ xl yl ∗ big_sepHL_1 Φ xl' yl'.
-Proof. induction xl, yl; by [rewrite/= left_id|rewrite/= IHxl assoc]. Qed.
+Proof. induction xl as [|X Xl x xl IH], yl; by [rewrite/= left_id|rewrite/= IH assoc]. Qed.
 
 Global Instance into_sep_big_sepHL_app {F: A → Type} {Xl Yl}
     (xl: hlist F Xl) (xl': hlist F Yl) (Φ: ∀C, F C → PROP) :
@@ -714,8 +717,8 @@ Lemma big_sepHL_2_big_sepN {F G H: A → Type} {Xl}
   big_sepHL_2 Φ xl yl zl ⊣⊢
   [∗ nat] i < length Xl, Φ _ (xl +!! i) (yl -!! i) (zl -!! i).
 Proof.
-  move: Φ. induction Xl; inv_hlist xl; case yl; case zl; [done|]=>/= *.
-  f_equiv; [done|apply IHXl].
+  move: Φ. induction Xl as [|X Xl IH]; inv_hlist xl; case yl; case zl; [done|]=>/= *.
+  f_equiv; [done|apply IH].
 Qed.
 
 Lemma big_sepHL_2_lookup {F G H: A → Type} {Xl}
diff --git a/theories/util/vector.v b/theories/util/vector.v
index 95107ddf..17d6a8e1 100644
--- a/theories/util/vector.v
+++ b/theories/util/vector.v
@@ -37,7 +37,7 @@ Notation vzip := (vzip_with pair).
 
 Lemma vzip_with_app {A B C m n} (f: A → B → C) (xl: vec _ m) (xl': vec _ n) yl yl' :
   vzip_with f (xl +++ xl') (yl +++ yl') = vzip_with f xl yl +++ vzip_with f xl' yl'.
-Proof. induction xl; inv_vec yl; [done|]=>/= ??. by rewrite IHxl. Qed.
+Proof. induction xl as [|x m xl IH]; inv_vec yl; [done|]=>/= ??. by rewrite IH. Qed.
 
 (** [vsepat] *)
 
@@ -46,8 +46,8 @@ Notation vsepat := Vector.splitat.
 Lemma vsepat_app {A m n} (xl: _ A (m + n)) :
   xl = (vsepat m xl).1 +++ (vsepat m xl).2.
 Proof.
-  induction m; [done|]=>/=.
-  by rewrite [vsepat _ _]surjective_pairing /= -IHm -surjective_vcons.
+  induction m as [|m IH]; [done|]=>/=.
+  by rewrite [vsepat _ _]surjective_pairing /= -IH -surjective_vcons.
 Qed.
 Lemma vapp_ex {A m n} (xl: _ A (m + n)) : ∃yl zl, xl = yl +++ zl.
 Proof. eexists _, _. apply vsepat_app. Qed.
@@ -56,8 +56,8 @@ Global Instance vapp_vsepat_iso {A} m n : Iso (uncurry vapp) (@vsepat A m n).
 Proof.
   split; fun_ext.
   - move=> [xl ?]. by elim xl; [done|]=>/= ???->.
-  - move=>/= ?. rewrite [vsepat _ _]surjective_pairing /=. induction m; [done|]=>/=.
-    by rewrite [vsepat _ _]surjective_pairing /= IHm -surjective_vcons.
+  - move=>/= ?. rewrite [vsepat _ _]surjective_pairing /=. induction m as [|m IH]; [done|]=>/=.
+    by rewrite [vsepat _ _]surjective_pairing /= IH -surjective_vcons.
 Qed.
 
 (** [vsnoc] *)
@@ -86,7 +86,7 @@ Proof. by induction fl; inv_fin i. Qed.
 Global Instance vapply_vfunsep_iso {A B n} : Iso (@vapply A B n) vfunsep.
 Proof.
   split; fun_ext; [by elim; [done|]=>/= ???->|]. move=> f. fun_ext=>/= x.
-  induction n=>/=; [|rewrite IHn /=]; move: (f x)=> xl; by inv_vec xl.
+  induction n as [|n IH]=>/=; [|rewrite IH /=]; move: (f x)=> xl; by inv_vec xl.
 Qed.
 
 Lemma vapply_funsep {A B n} (f: B → vec A n) : vapply (vfunsep f) = f.
-- 
GitLab