diff --git a/gpfsl-examples/history/history.v b/gpfsl-examples/history/history.v
index 9c3d322a604505042d9d2cd20c5da9e600d10089..c4cb9d2431fd8888101c27a72f1020135793eae6 100644
--- a/gpfsl-examples/history/history.v
+++ b/gpfsl-examples/history/history.v
@@ -150,8 +150,8 @@ Proof.
     [hb_ord E l2], which implies [hb_ord E l1] by IH. Then add [x]. *)
     inversion EVs as [|?? [eV' EV'] EVs'].
     specialize (hb_ord_cons_inv _ _ _ _ EV' HB_ORD2); i; des.
-    lazymatch goal with [ X : hb_ord E _ |- _] => rename X into HB_ORD' end.
-    lazymatch goal with [ X : Forall (λ _, _ ∉ _) _ |- _] => rename X into NO_REV_HB end.
+    rename select (hb_ord E _) into HB_ORD'.
+    rename select (Forall (λ _, _ ∉ _) _) into NO_REV_HB.
     rewrite ->Forall_lookup in NO_REV_HB.
     specialize (IH EVs' HB_ORD').
     unfold hb_ord in IH |- *. intros i1 i2 e1 e2 eV2 ORD_i1 ORD_i2 EV2. intros.
diff --git a/gpfsl-examples/stack/proof_treiber_history.v b/gpfsl-examples/stack/proof_treiber_history.v
index ce1921eb2ca36527fc7df1574132dc40070bde7c..351552c88d79086b056f33dcc9dfd2325beeb743 100644
--- a/gpfsl-examples/stack/proof_treiber_history.v
+++ b/gpfsl-examples/stack/proof_treiber_history.v
@@ -2348,7 +2348,7 @@ Proof.
       rewrite ORD in XO_INTERP. by apply EMPTYING_POP in XO_INTERP.
     + (* The last (non-empty) event was empty pop: contradiction. *)
       exfalso.
-      lazymatch goal with [ X : ge_event eV = EmpPop |- _] => rename X into EMPPOP end.
+      rename select (ge_event eV = EmpPop) into EMPPOP.
       clear -ORD EVENT EMPPOP.
       assert (H: e ∈ ord' ++ [e]) by set_solver-.
       rewrite <- ORD in H.
diff --git a/gpfsl-examples/stack/spec_history.v b/gpfsl-examples/stack/spec_history.v
index f74aa8cee6b49337af5b1946af5bf2295c6ada2f..a84240996e50669412bf92c20a8106d42e94ad93 100644
--- a/gpfsl-examples/stack/spec_history.v
+++ b/gpfsl-examples/stack/spec_history.v
@@ -354,9 +354,8 @@ Proof.
   intros e ord IH stk1 stk2 INTERP ORD_NODUP.
   set (u := node.1.1.1) in *.
   inv INTERP; simplify_list_eq2.
-  lazymatch goal with [ X : event_id |- _] => rename X into e end.
-  lazymatch goal with [ X : stack_run e _ _ _ |- _] => rename X into RUN end.
-
+  rename select (event_id) into e.
+  rename select (stack_run e _ _ _) into RUN.
   apply NoDup_app in ORD_NODUP as (ORD_NODUP' & NOT_IN & _).
   case (decide (u = e)) as [<-|NE].
   - (* the last event pushed [node] *) inv RUN; simplify_list_eq2.
@@ -364,27 +363,21 @@ Proof.
       { (* no duplicate push id *) exfalso. simplify_list_eq.
         exploit stack_node_ids; [done..|].
         rewrite !fmap_app !fmap_cons /=. i. des. set_solver. }
-      (* apply eq_sym in H3 as Hnode; clear H3. simplify_list_eq. *)
-      (* rewrite H /=. exists eV. *)
-      lazymatch goal with [ X : graph_event _ |- _] => rename X into eV end.
       simplify_list_eq.
-      exists eV. destruct node as [[[??]?]?]; simplify_eq.
+      eexists. destruct node as [[[??]?]?]; simplify_eq.
       split_and!; red; [set_solver|done..].
     + (* pop *)
-      lazymatch goal with [ X : stack_interp _ _ _ _ |- _] => rename X into INTERP' end.
-      lazymatch goal with [ X : graph_event _ |- _] => rename X into eV end.
+      rename select (stack_interp _ _ _ _) into INTERP'.
       specialize (IH (_ :: stk1) _ INTERP' ORD_NODUP'). des.
-      exists eV. split_and!; red; set_solver.
+      eexists. split_and!; red; set_solver.
   - inv RUN; simpl in *; simplify_list_eq2.
     + case Estk1: stk1 => [|? stk1']; simplify_list_eq.
-      lazymatch goal with [ X : stack_interp _ _ _ _ |- _] => rename X into INTERP' end.
+      rename select (stack_interp _ _ _ _) into INTERP'.
       specialize (IH _ _ INTERP' ORD_NODUP'). des.
-      lazymatch goal with [H_ : context[E !! u = Some ?X] |- _] => rename X into uV end.
-      exists uV. split_and!; red; [set_solver|try done..].
-    + lazymatch goal with [ X : stack_interp _ _ _ _ |- _] => rename X into INTERP' end.
+      eexists. split_and!; red; [set_solver|done..].
+    + rename select (stack_interp _ _ _ _) into INTERP'.
       specialize (IH (_ :: stk1) _ INTERP' ORD_NODUP'). des.
-      lazymatch goal with [H_ : context[E !! u = Some ?X] |- _] => rename X into uV end.
-      exists uV. split_and!; red; [set_solver|done..].
+      eexists. split_and!; red; [set_solver|done..].
 Qed.
 
 Lemma stack_interp_nil_inv E stk stk'
diff --git a/gpfsl/base_logic/base_lifting.v b/gpfsl/base_logic/base_lifting.v
index 7a79d003d79bf14223afb71c48f5aa0985ab32c5..1d837685337ca06ede892c502ce0990a7829c211 100644
--- a/gpfsl/base_logic/base_lifting.v
+++ b/gpfsl/base_logic/base_lifting.v
@@ -132,9 +132,9 @@ Proof.
   - iIntros (v2 σ2 efs Hstep) "_"; inv_head_step.
     (* accessing hist_ctx *)
     iMod (hist_interp_open _ _ SUB with "Hσ") as "[Hσ HClose]".
-    lazymatch goal with [ X : drf_post _ _ _ _ _ |- _] => rename X into DRFPost end.
-    lazymatch goal with [ X : lbl_machine_step _ _ _ _ _ _ _ _ _ |- _] => rename X into PStep end.
-    lazymatch goal with [ X : option positive |- _] => rename X into ot end.
+    rename select (drf_post _ _ _ _ _) into DRFPost.
+    rename select (lbl_machine_step _ _ _ _ _ _ _ _ _) into PStep.
+    rename select (option positive) into ot.
     have ?: ot = None by inversion DRFPost. subst ot.
     iMod (hist_ctx_alloc _ (mkGB _ _ _) _ _ _ _ _ PStep with "Hσ")
       as "(Hσ' & hF & Hists & Hars & Haws & Hnas & Seen' & Ext)";
@@ -146,7 +146,7 @@ Proof.
       by rewrite -Z2Nat.inj_pos Z2Pos.id.
     rewrite Eqn. iFrame.
     inversion_clear PStep.
-    lazymatch goal with [ X : alloc_step _ _ _ _ _ _ _ |- _] => rename X into ALLOC end.
+    rename select (alloc_step _ _ _ _ _ _ _) into ALLOC.
     rewrite Eqn /= in ALLOC.
     rewrite cell_list_fmap big_sepL_fmap /=.
     rewrite (_:∀ n l, (l ↦∗{1} repeat #☠ n) ⊣⊢
@@ -163,7 +163,7 @@ Proof.
     rewrite -4!big_sepL_sep monPred_at_big_sepL.
     iApply (big_sepL_mono with "Hists").
     move => n1 n2 /lookup_seq [/= -> Lt].
-    lazymatch goal with [ X : list message |- _] => rename X into 𝑚s end.
+    rename select (list message) into 𝑚s.
     destruct (lookup_lt_is_Some_2 𝑚s n1) as [𝑚 Eq𝑚];
       first by rewrite (alloc_step_length _ _ _ _ _ _ _ ALLOC).
     rewrite -(alloc_step_loc_eq _ _ _ _ _ _ _ ALLOC _ _ Eq𝑚)
@@ -220,10 +220,10 @@ Proof.
   - iNext. iIntros (v2 σ2 efs Hstep) "_"; inv_head_step.
     (* accessing hist_ctx *)
     iMod (hist_interp_open _ _ SUB with "Hσ") as "[Hσ HClose]".
-    lazymatch goal with [ X : drf_post _ _ _ _ _ |- _] => rename X into DRFPost end.
+    rename select (drf_post _ _ _ _ _) into DRFPost.
     lazymatch goal with [ X : context[drf_pre _ _ _ _] |- _] => rename X into DRFPre end.
-    lazymatch goal with [ X : lbl_machine_step _ _ _ _ _ _ _ _ _ |- _] => rename X into PStep end.
-    lazymatch goal with [ X : option positive |- _] => rename X into ot end.
+    rename select (lbl_machine_step _ _ _ _ _ _ _ _ _) into PStep.
+    rename select (option positive) into ot.
     have ?: ot = None by inversion DRFPost. subst ot.
     iMod (hist_ctx_dealloc _ (mkGB _ _ _) _ _ _ _ _ PStep with "[$Hσ Hmt]")
       as "(Hσ' & seen' & Ext)"; [|done|done|apply WF|..|done| |].
@@ -298,9 +298,9 @@ Proof.
   (* accessing hist_ctx *)
   iMod (hist_interp_open _ _ SUB with "Hσ") as "[Hσ HClose]".
   iDestruct (hist_ctx_read with "Hσ hist") as "#VS".
-  lazymatch goal with [ X : drf_post _ _ _ _ _ |- _] => rename X into DRFPost end.
-  lazymatch goal with [ X : option positive |- _] => rename X into ot end.
-  lazymatch goal with [ X : list message |- _] => rename X into 𝑚s end.
+  rename select (drf_post _ _ _ _ _) into DRFPost.
+  rename select (option positive) into ot.
+  rename select (list message) into 𝑚s.
 
   assert (∃ tr, ot = Some tr ∧ 𝑚s = []) as [tr [? ?]].
   { inversion_clear DRFPost. by eexists. } subst ot 𝑚s.
@@ -443,9 +443,9 @@ Proof.
   iModIntro. iSplit; [done|].
   iIntros (v2 σ2 efs Hstep) "!> _"; inv_head_step.
 
-  lazymatch goal with [ X : drf_post _ _ _ _ _ |- _] => rename X into DRFPost end.
-  lazymatch goal with [ X : option positive |- _] => rename X into ot end.
-  lazymatch goal with [ X : list message |- _] => rename X into 𝑚s end.
+  rename select (drf_post _ _ _ _ _) into DRFPost.
+  rename select (option positive) into ot.
+  rename select (list message) into 𝑚s.
   lazymatch goal with [ X : context[drf_pre _ _ _ _] |- _] => rename X into DRFPre end.
 
   assert (∃ 𝑚, ot = None ∧ 𝑚s = [𝑚]) as [𝑚 [? ?]].
@@ -637,9 +637,9 @@ Proof.
   (* done accessing hist_ctx *)
   iModIntro. iSplit; [done|]. iIntros (v2 σ2 efs Hstep) "_"; inv_head_step.
   - iClear "VSC".
-    lazymatch goal with [ X : drf_post _ _ _ _ _ |- _] => rename X into DRFPost end.
-    lazymatch goal with [ X : option positive |- _] => rename X into ot end.
-    lazymatch goal with [ X : list message |- _] => rename X into 𝑚s end.
+    rename select (drf_post _ _ _ _ _) into DRFPost.
+    rename select (option positive) into ot.
+    rename select (list message) into 𝑚s.
 
     assert (∃ tr, ot = Some tr ∧ 𝑚s = []) as [tr [? ?]].
     { inversion_clear DRFPost. by eexists. } subst ot 𝑚s.
@@ -661,9 +661,9 @@ Proof.
     iMod ("HΦ" with "[%//] P seen' hist ar na aw [%//]") as "HΦ".
     iIntros "!> !>". by iMod "HΦ" as "$".
   - iClear "VSR".
-    lazymatch goal with [ X : drf_post _ _ _ _ _ |- _] => rename X into DRFPost end.
-    lazymatch goal with [ X : option positive |- _] => rename X into ot end.
-    lazymatch goal with [ X : list message |- _] => rename X into 𝑚s end.
+    rename select (drf_post _ _ _ _ _) into DRFPost.
+    rename select (option positive) into ot.
+    rename select (list message) into 𝑚s.
     lazymatch goal with [ X : context[drf_pre _ _ _ _] |- _] => rename X into DRFPre end.
 
     assert (∃ tr 𝑚, ot = Some tr ∧ 𝑚s = [𝑚]) as [tr [𝑚 [? ?]]].
@@ -744,10 +744,10 @@ Proof.
     iMod (hist_interp_open _ _ SUB with "Hσ") as "[Hσ HClose]".
     iDestruct (hist_ctx_seen_wf with "Hσ seen") as %(WF & HC).
 
-    lazymatch goal with [ X : drf_post _ _ _ _ _ |- _] => rename X into DRFPost end.
-    lazymatch goal with [ X : lbl_machine_step _ _ _ _ _ _ _ _ _ |- _] => rename X into PStep end.
-    lazymatch goal with [ X : option positive |- _] => rename X into ot end.
-    lazymatch goal with [ X : list message |- _] => rename X into 𝑚s end.
+    rename select (drf_post _ _ _ _ _) into DRFPost.
+    rename select (lbl_machine_step _ _ _ _ _ _ _ _ _) into PStep.
+    rename select (option positive) into ot.
+    rename select (list message) into 𝑚s.
     lazymatch goal with [ X : drf_post _ _ _ _ ?V |- _] => rename V into 𝓝' end.
     lazymatch goal with [ X : lbl_machine_step _ _ _ _ _ _ _ ?M ?Ss |- _] =>
       rename M into M'; rename Ss into 𝓢' end.
@@ -777,10 +777,10 @@ Proof.
     iMod (hist_interp_open _ _ SUB with "Hσ") as "[Hσ HClose]".
     iDestruct (hist_ctx_seen_wf with "Hσ seen") as %(WF & HC).
 
-    lazymatch goal with [ X : drf_post _ _ _ _ _ |- _] => rename X into DRFPost end.
-    lazymatch goal with [ X : lbl_machine_step _ _ _ _ _ _ _ _ _ |- _] => rename X into PStep end.
-    lazymatch goal with [ X : option positive |- _] => rename X into ot end.
-    lazymatch goal with [ X : list message |- _] => rename X into 𝑚s end.
+    rename select (drf_post _ _ _ _ _) into DRFPost.
+    rename select (lbl_machine_step _ _ _ _ _ _ _ _ _) into PStep.
+    rename select (option positive) into ot.
+    rename select (list message) into 𝑚s.
     lazymatch goal with [ X : drf_post _ _ _ _ ?V |- _] => rename V into 𝓝' end.
     lazymatch goal with [ X : lbl_machine_step _ _ _ _ _ _ _ ?M ?Ss |- _] =>
       rename M into M'; rename Ss into 𝓢' end.
@@ -810,10 +810,10 @@ Proof.
     iMod (hist_interp_open _ _ SUB with "Hσ") as "[Hσ HClose]".
     iDestruct (hist_ctx_seen_wf with "Hσ seen") as %(WF & HC).
 
-    lazymatch goal with [ X : drf_post _ _ _ _ _ |- _] => rename X into DRFPost end.
-    lazymatch goal with [ X : lbl_machine_step _ _ _ _ _ _ _ _ _ |- _] => rename X into PStep end.
-    lazymatch goal with [ X : option positive |- _] => rename X into ot end.
-    lazymatch goal with [ X : list message |- _] => rename X into 𝑚s end.
+    rename select (drf_post _ _ _ _ _) into DRFPost.
+    rename select (lbl_machine_step _ _ _ _ _ _ _ _ _) into PStep.
+    rename select (option positive) into ot.
+    rename select (list message) into 𝑚s.
     lazymatch goal with [ X : drf_post _ _ _ _ ?V |- _] => rename V into 𝓝' end.
     lazymatch goal with [ X : lbl_machine_step _ _ _ _ _ _ _ ?M ?Ss |- _] =>
       rename M into M'; rename Ss into 𝓢' end.
@@ -829,7 +829,7 @@ Proof.
     iModIntro; iSplit; [done|].
     iApply "HΦ". iFrame. iPureIntro. split; [done|]. eexists. split; [done|].
     inversion PStep.
-    lazymatch goal with [ X : sc_fence_step _ _ _ _ |- _] => inversion X end.
+    destruct select (sc_fence_step _ _ _ _).
     by subst.
 Qed.
 
@@ -848,10 +848,10 @@ Proof.
     iMod (hist_interp_open _ _ SUB with "Hσ") as "[Hσ HClose]".
     iDestruct (hist_ctx_seen_wf with "Hσ seen") as %(WF & HC).
 
-    lazymatch goal with [ X : drf_post _ _ _ _ _ |- _] => rename X into DRFPost end.
-    lazymatch goal with [ X : lbl_machine_step _ _ _ _ _ _ _ _ _ |- _] => rename X into PStep end.
-    lazymatch goal with [ X : option positive |- _] => rename X into ot end.
-    lazymatch goal with [ X : list message |- _] => rename X into 𝑚s end.
+    rename select (drf_post _ _ _ _ _) into DRFPost.
+    rename select (lbl_machine_step _ _ _ _ _ _ _ _ _) into PStep.
+    rename select (option positive) into ot.
+    rename select (list message) into 𝑚s.
     lazymatch goal with [ X : drf_post _ _ _ _ ?V |- _] => rename V into 𝓝' end.
     lazymatch goal with [ X : lbl_machine_step _ _ _ _ _ _ _ ?M ?Ss |- _] =>
       rename M into M'; rename Ss into 𝓢' end.
@@ -866,7 +866,7 @@ Proof.
     iModIntro; iSplit; [done|].
     iApply "HΦ". iFrame. iPureIntro. split; [done|]. eexists.
     inversion PStep.
-    lazymatch goal with [ X : sc_fence_step _ _ _ _ |- _] => inversion X end.
+    destruct select (sc_fence_step _ _ _ _).
     by subst.
 Qed.
 
diff --git a/gpfsl/base_logic/history.v b/gpfsl/base_logic/history.v
index 87b04e46f0d02d0b68609eab7ff60add77cd1aa7..b665547bf2dedf54f08a07eb9d9d1a0b04f74a67 100644
--- a/gpfsl/base_logic/history.v
+++ b/gpfsl/base_logic/history.v
@@ -836,7 +836,7 @@ Section hist.
           own hist_naread_name (◯ {[l >> i := (1%Qp, to_latT ∅)]}))).
   Proof.
     inversion_clear STEP.
-    lazymatch goal with [ X : alloc_step _ _ _ _ _ _ _ |- _] => rename X into ALLOC end.
+    rename select (alloc_step _ _ _ _ _ _ _) into ALLOC.
     have FRESH := alloc_step_mem_fresh _ _ _ _ _ _ _ ALLOC.
     rewrite -(alloc_step_length _ _ _ _ _ _ _ ALLOC) in FRESH.
     have DISJ := alloc_step_disjoint  _ _ _ _ _ _ _ ALLOC.
@@ -932,8 +932,7 @@ Section hist.
     have FRESH: ∀ m, σ.(mem) !!c (l.1, m) = ∅.
     { move => ?. rewrite memory_cell_lookup_empty.
       inversion_clear STEP.
-      lazymatch goal with [ X : alloc_step _ _ _ _ _ _ _ |- _] =>
-        inversion X as [?? MEMALL] end. apply MEMALL. }
+      destruct select (alloc_step _ _ _ _ _ _ _)  as [?? MEMALL]. apply MEMALL. }
     iMod (hist_ctx_alloc_vs _ _ _ _ _ _ _ _ _ _ _ _ STEP DRFPost LE
       with "[$Hhσ $Har $Haw $Hna]") as (Vc' LE')
         "((Hhσ'&Hh) & (Har'&Har) & (Haw'&Haw) & Hna' & Hn)"; [apply WF..|].
@@ -992,7 +991,7 @@ Section hist.
           ∗ ([∗ list] i ∈ seq 0 (Pos.to_nat n), naread (l >> i) 1 ∅)).
   Proof.
     inversion_clear STEP. subst. simpl in *.
-    lazymatch goal with [ X : dealloc_step _ _ _ _ _ _ _ |- _] => rename X into DEALLOC end.
+    rename select (dealloc_step _ _ _ _ _ _ _) into DEALLOC.
     have DISJ := dealloc_step_disjoint  _ _ _ _ _ _ _ DEALLOC.
     inversion_clear DEALLOC as [??? MEMALL VALL].
     inversion_clear MEMALL as [LEN DMES ADD' DEALLOC]. inversion_clear DRFPost.
@@ -1195,8 +1194,7 @@ Section hist.
       have Eq𝑚 : C !! 𝑚.(mto) = Some 𝑚.(mbase).
       { rewrite EqC cell_cut_lookup_Some -memory_lookup_cell. split; [done|].
         change (Some t ⊑ Some 𝑚.(mto)).
-        lazymatch goal with [ X : read_helper _ _ _ _ _ _ _ |- _] =>
-          rename X into READ end.
+        rename select (read_helper _ _ _ _ _ _ _) into READ.
         etrans; last (inversion READ as [PLN]; apply PLN).
         destruct ALL as (t'&m'&Eqt'&Eqv'&SL'). etrans; last apply SL'.
         apply (cell_cut_lookup_Some (σ.(mem) !!c 𝑚.(mloc)) _ _ m').
@@ -1674,8 +1672,7 @@ Section hist.
       inversion_clear X as [? POST] end.
     simplify_eq.
     set 𝓝2 := (add_aread_id (na σ) (mloc 𝑚) tr). destruct POST as [POST1 POST2].
-    lazymatch goal with [ X : mloc _ = mloc 𝑚 |- _] =>
-      rename X into SAMEM end.
+    rename select (mloc _ = mloc 𝑚) into SAMEM.
     iDestruct ("VS" $! (mkGB σ'.(sc) σ'.(na) σ'.(mem)) 𝓥 𝓥2 𝓥' 𝓝2 𝑚1 𝑚 with "[%] AR AW")
       as (C') "{VS} [FACTS VS]".
     { rewrite SAMEM. do 7 (split; [done|]). split.
@@ -1715,14 +1712,14 @@ Section hist.
       assert (SL:= write_helper_seen_local_write RLXW WH).
       clear -NEQ SL. rewrite /seen_local in SL. intros Eq. rewrite Eq in NEQ.
       apply : (irreflexivity (⊏) (_ !!w _)). eapply strict_transitive_l; eauto. } split.
-    { assert (FR := write_helper_fresh WH). rewrite SAME. clear -Ext1 FR.
+    { assert (FR := write_helper_fresh WH). rewrite SAMEM. clear -Ext1 FR.
       eapply strict_transitive_r; by [apply view_sqsubseteq, Ext1|]. } split.
-    { by rewrite SAME. } split.
-    { by rewrite SAME. } split.
+    { by rewrite SAMEM. } split.
+    { by rewrite SAMEM. } split.
     { clear -LEt NEQ. intros Le. apply : (irreflexivity (⊏) (_ !!w _)).
       eapply strict_transitive_l; [|exact LEt]. eapply strict_transitive_r; [|exact NEQ].
       by apply view_sqsubseteq, Le. }
-    repeat split; [done|..|by rewrite SAME].
+    repeat split; [done|..|by rewrite SAMEM].
     - case decide => [?|//]. subst or.
       by apply (write_helper_acq_tview_include WH), (read_helper_view_relaxed RH).
     - case decide => [?|//]. subst or.
@@ -1748,7 +1745,7 @@ Section hist.
     - iDestruct (seen_own_join with "HV") as "$".
       iPureIntro. split; [done|].
       inversion STEP.
-      lazymatch goal with [ X : acq_fence_step _ _ |- _] => by inversion X end.
+      by destruct select (acq_fence_step _ _).
   Qed.
 
   Lemma hist_ctx_rel_fence σ 𝓥 𝓥'
@@ -1769,7 +1766,7 @@ Section hist.
       by apply (machine_step_view_join_update _ _ _ _ _ _ _ _ STEP).
     - iDestruct (seen_own_join with "HV") as "$".
       iPureIntro. split; [done|].
-      lazymatch goal with [ X : rel_fence_step _ _ |- _] => by inversion X end.
+      by destruct select (rel_fence_step _ _).
   Qed.
 
   Lemma hist_ctx_sc_fence σ σ' 𝓥 𝓥' 𝓢
@@ -1784,8 +1781,8 @@ Section hist.
     iDestruct "Hσ" as (hF V ?) "(Hhσ & HhF & Hna & Haw & Hat & HSC & HV & HF)".
     iDestruct "HF" as %(WF & HhF & HC & ?).
     inversion STEP. subst.
-    lazymatch goal with [ X : sc_fence_step _ _ _ _ |- _] => rename X into FSC end.
-    match goal with H : mem _ = mem _ |- _ => rename H into Eqm end.
+    rename select (sc_fence_step _ _ _ _) into FSC.
+    rename select (mem _ = mem _) into Eqm.
     have ?: σ.(sc) ⊑ σ'.(sc).
     { inversion FSC. by eapply sc_fence_helper_sc_sqsubseteq. }
     iMod (own_lat_auth_update _ _ σ'.(sc) with "HSC") as "[HSC SC']"; first done.
@@ -1812,8 +1809,8 @@ Section hist.
     iDestruct 1 as (hF V ?) "(Hhσ & HhF & Hna & Haw & Hat & HSC & HV & HF)".
     iDestruct "HF" as %(WF & HhF & HC & ?).
     inversion STEP. subst.
-    lazymatch goal with [ X : sc_fence_step _ _ _ _ |- _] => rename X into FSC end.
-    match goal with H : mem _ = mem _ |- _ => rename H into Eqm end.
+    rename select (sc_fence_step _ _ _ _) into FSC.
+    rename select (mem _ = mem _) into Eqm.
     have ?: σ.(sc) ⊑ σ'.(sc).
     { inversion FSC. by eapply sc_fence_helper_sc_sqsubseteq. }
     iMod (own_lat_auth_update _ _ σ'.(sc) with "HSC") as "[HSC SC']"; first done.
diff --git a/gpfsl/base_logic/weakestpre.v b/gpfsl/base_logic/weakestpre.v
index 19648d1c9d17de3e5c3e74bd9688bc27dc70d85b..52f19dc32c84148234d6546907012c19133b1aa0 100644
--- a/gpfsl/base_logic/weakestpre.v
+++ b/gpfsl/base_logic/weakestpre.v
@@ -28,15 +28,15 @@ Lemma hist_head_step_seen e e' efs 𝓥 𝓥' σ σ' κs
 Proof.
   iIntros (STEP) "ctx #s". inv_head_step.
   - iFrame "ctx #".
-    lazymatch goal with [ X : head_step _ _ _ _ _ _ |- _] => rename X into BaseStep end.
+    rename select (head_step _ _ _ _ _ _) into BaseStep.
     destruct efs as [|?[]]; inversion BaseStep; subst=>//=.
-    lazymatch goal with [ X : Forall _ _ |- _] => rename X into ForkViews end.
+    rename select (Forall _ _) into ForkViews.
     inversion ForkViews as [|? ? Eq1]. subst. rewrite -Eq1.
     by iDestruct (seen_mono _ _ (nopro_lang.forkView_subseteq _) with "s") as "$".
   - iDestruct "ctx" as (hF V Vc) "(MEM & HF & NA & AW & AR & SC & VT & WF)".
     iDestruct "WF" as %(WFs & HRel & IN' & LE).
     iMod (own_lat_auth_update_join _ V (𝓥'.(acq)) with "VT") as "[VT VTo]".
-    lazymatch goal with [ X : lbl_machine_step _ _ _ _ _ _ _ _ _ |- _] => rename X into PStep end.
+    rename select (lbl_machine_step _ _ _ _ _ _ _ _ _) into PStep.
     have INV' := machine_step_closed_tview _ _ _ _ _ _ _ _ _ PStep
                     (global_wf_mem _ WF) IN (global_wf_sc _ WF).
     iDestruct (seen_own_join with "VTo") as "$".
diff --git a/gpfsl/lang/lang.v b/gpfsl/lang/lang.v
index d6dfd2045f53ba145a362dc2122e75ce025db2a5..e4117d0e3251c65389aadd05a1d08acde9e74831 100644
--- a/gpfsl/lang/lang.v
+++ b/gpfsl/lang/lang.v
@@ -463,10 +463,10 @@ Module base.
   Proof.
     revert e X Y. fix FIX 1; intros [] X Y; try naive_solver.
     - naive_solver set_solver.
-    - lazymatch goal with [ X : list expr |- _] => rename X into el end.
+    - rename select (list expr) into el.
       rewrite !andb_True. intros [He Hel] HXY. split; first by eauto.
       induction el=>/=; naive_solver.
-    - lazymatch goal with [ X : list expr |- _] => rename X into el end.
+    - rename select (list expr) into el. 
       rewrite !andb_True. intros [He Hel] HXY. split; first by eauto.
       induction el=>/=; naive_solver.
   Qed.
@@ -479,10 +479,10 @@ Module base.
     revert e X. fix FIX 1; intros [] X; rewrite /= ?bool_decide_spec ?andb_True=> He ?;
       repeat case_bool_decide; simplify_eq/=; f_equal;
       try by intuition eauto with set_solver.
-    - lazymatch goal with [ X : list expr |- _] => rename X into el end.
+    - rename select (list expr) into el. 
       case He=> _. clear He. induction el=>//=. rewrite andb_True=>?.
       f_equal; intuition eauto with set_solver.
-    - lazymatch goal with [ X : list expr |- _] => rename X into el end.
+    - rename select (list expr) into el. 
       case He=> _. clear He. induction el=>//=. rewrite andb_True=>?.
       f_equal; intuition eauto with set_solver.
   Qed.
@@ -500,13 +500,12 @@ Module base.
       try naive_solver; rewrite ?andb_True; intros.
     - set_solver.
     - eauto using is_closed_weaken with set_solver.
-    - lazymatch goal with [ X : binder |- _] => rename X into f end.
-      lazymatch goal with [ X : list binder |- _] => rename X into xl end.
+    - rename select (binder) into f. rename select (list binder) into xl.
       eapply is_closed_weaken; first done.
       destruct (decide (BNamed x = f)), (decide (BNamed x ∈ xl)); set_solver.
-    - lazymatch goal with [ X : list expr |- _] => rename X into el end.
+    - rename select (list expr) into el. 
       split; first naive_solver. induction el; naive_solver.
-    - lazymatch goal with [ X : list expr |- _] => rename X into el end.
+    - rename select (list expr) into el. 
       split; first naive_solver. induction el; naive_solver.
   Qed.
 
@@ -653,8 +652,7 @@ Module base.
        | GenNode 15 [e1; e2] => Free (go e1) (go e2)
        | _ => Lit LitPoison
        end) _).
-    fix FIX 1. intros []; f_equal=>//;
-      lazymatch goal with [ X : list expr |- _] => revert X end; clear -FIX.
+    fix FIX 1. intros []; f_equal=>//; revert select (list expr); clear -FIX.
     - fix FIX_INNER 1. intros []; [done|]. by simpl; f_equal.
     - fix FIX_INNER 1. intros []; [done|]. by simpl; f_equal.
   Qed.
@@ -812,7 +810,7 @@ Module nopro_lang.
     head_step e1 σ1 κs e2 σ2 ef → to_val e1 = None.
   Proof.
     inversion 1; subst;
-      last (lazymatch goal with [ X : base.head_step _ _ _ _ _ _ |- _] => inversion X end);
+      last destruct select (base.head_step _ _ _ _ _ _);
       first (cbv -[base.to_val]; by erewrite val_stuck; last eassumption);
       reflexivity.
   Qed.
@@ -943,8 +941,7 @@ Section Progress.
     - constructor.
       destruct v eqn:Eqv; [apply memval_val_AVal| |apply memval_val_VVal].
       inversion RS. subst.
-      lazymatch goal with [ X : read_step _ _ _ _ _ _ |- _] =>
-        inversion X as [? IN] end.
+      destruct select (read_step _ _ _ _ _ _) as [? IN].
       by specialize (ALLOC _ _ IN).
     - done.
     - clear DRF RS ISVAL. move => evt2 e2 efs2 ots 𝑚s2 𝓥2 M2 𝓢2 STEP' MSTEP'.
@@ -1014,11 +1011,8 @@ Section Progress.
     - exists (mkGB σ.(sc) 𝓝' M'), 𝓥', false.
       econstructor 2;  [done| |done|by constructor|..].
       + inversion READ.
-        lazymatch goal with [ X : mval (mbase _) = VVal v |- _] =>
-          rename X into EqV end.
-        lazymatch goal with [ X : read_step _ _ _ _ _ _ |- _] =>
-          inversion X as [READ' IN] end.
-        inversion READ' as [PLN]. subst.
+        rename select (mval (mbase _) = VVal v) into EqV.
+        destruct select (read_step _ _ _ _ _ _) as [[PLN] IN]. subst.
         destruct (NUB _ _ IN PLN) as [v0 [REL Comp0]].
         inversion REL as [? EqV'|]; subst; [|by inversion Comp0].
         eapply CasFailS; [eauto..| |done]. rewrite EqV in EqV'.
@@ -1028,19 +1022,15 @@ Section Progress.
         move => evt2 e2 efs2 ots 𝑚s2 𝓥2 M2 𝓢2 STEP' MSTEP'. inversion STEP'.
         * subst. simplify_eq. constructor. clear - DRFR RLXR.
           inversion DRFR; subst.
-          lazymatch goal with [ X : drf_pre_read _ _ _ _ _ |- _] =>
-            inversion X end.
+          destruct select (drf_pre_read _ _ _ _ _).
           constructor; [done|]. by rewrite (decide_True _ _ RLXR).
         * subst. simplify_eq. clear -DRFR. inversion DRFR; subst.
           by constructor.
     - exists (mkGB σ.(sc) 𝓝' M'), 𝓥', true. subst l.
       econstructor 2; [done| |done|by constructor|..].
       + inversion UPDATE.
-        lazymatch goal with [ X : read_step _ _ _ _ _ _ |- _] =>
-          inversion X as [READ' IN] end.
-        inversion READ' as [PLN]. subst.
-        lazymatch goal with [ X : mloc _ = mloc 𝑚 |- _] =>
-          rename X into SAMEM end. rewrite -SAMEM in NUB.
+        destruct select (read_step _ _ _ _ _ _) as [[PLN] IN]. subst.
+        lazymatch goal with [ X : mloc _ = mloc 𝑚 |- _] => rewrite -X in NUB end.
         destruct (NUB _ _ IN PLN) as [v0 [Eq0 Comp0]].
         lazymatch goal with [ X : mval (mbase _) = VVal (LitV vr) |- _] =>
           rewrite X in Eq0 end. inversion Eq0. subst v0.
@@ -1049,8 +1039,7 @@ Section Progress.
         move => evt2 e2 efs2 ots 𝑚s2 𝓥2 M2 𝓢2 STEP' MSTEP'. inversion STEP'.
         * subst. simplify_eq. constructor. clear - DRFR RLXR.
           inversion DRFR; subst.
-          lazymatch goal with [ X : drf_pre_read _ _ _ _ _ |- _] =>
-            inversion X end.
+          destruct select (drf_pre_read _ _ _ _ _).
           constructor; [done|]. by rewrite (decide_True _ _ RLXR).
         * subst. simplify_eq. clear -DRFR. inversion DRFR; subst.
           by constructor.
diff --git a/gpfsl/lang/tactics.v b/gpfsl/lang/tactics.v
index e3ef1b0141b96ac3493cb1b5554573f14f093f2e..5139a7ab5734ca40960452fc0a095e850ed85107 100644
--- a/gpfsl/lang/tactics.v
+++ b/gpfsl/lang/tactics.v
@@ -101,10 +101,10 @@ Fixpoint is_closed (X : list string) (e : expr) : bool :=
 
 Lemma is_closed_correct X e : is_closed X e → base.is_closed X (to_expr e).
 Proof.
-  revert e X. fix FIX 1; destruct e =>/=;
+  revert e X. fix FIX 1; intros [] =>/=;
   try naive_solver eauto using is_closed_of_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]
@@ -156,10 +156,10 @@ Fixpoint subst (x : string) (es : expr) (e : expr)  : expr :=
 Lemma to_expr_subst x er e :
   to_expr (subst x er e) = base.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 [] => /= ? er; repeat case_bool_decide;
     f_equal; auto using is_closed_nil_subst, is_closed_of_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) :=
diff --git a/gpfsl/logic/lifting.v b/gpfsl/logic/lifting.v
index 3e7c478d4f71d99a6ae704851f020b47830b4fb7..c66927ae3e3b87011e58275d8d9c92c93c68d813 100644
--- a/gpfsl/logic/lifting.v
+++ b/gpfsl/logic/lifting.v
@@ -297,8 +297,7 @@ Proof.
   inv_head_step.
   lazymatch goal with [ X : lbl_machine_step _ _ _ _ _ _ _ _ _ |- _] =>
     inversion X end.
-  lazymatch goal with [ X : rel_fence_step _ _ |- _] =>
-    inversion X end. done.
+  by destruct select (rel_fence_step _ _).
 Qed.
 
 Global Instance elim_modal_wp_rel_fence (P : vProp Σ) tid E Φ p :
@@ -365,8 +364,7 @@ Proof.
   inv_head_step.
   lazymatch goal with [ X : lbl_machine_step _ _ _ _ _ _ _ _ _ |- _] =>
     inversion X end.
-  lazymatch goal with [ X : acq_fence_step _ _ |- _] =>
-    inversion X end. subst. simpl in *.
+  destruct select (acq_fence_step _ _). subst.
   change 𝓥'.(acq) with (acq_fence_tview 𝓥').(cur). by f_equiv.
 Qed.
 
@@ -424,10 +422,8 @@ Proof.
   inv_head_step.
   lazymatch goal with [ X : lbl_machine_step _ _ _ _ _ _ _ _ _ |- _] =>
     inversion X end.
-  lazymatch goal with [ X : sc_fence_step _ _ _ _ |- _] =>
-    inversion X end.
-  lazymatch goal with [ X : sc_fence_helper _ _ _ _ |- _] =>
-    inversion X end. done.
+  destruct select (sc_fence_step _ _ _ _).
+  by destruct select (sc_fence_helper _ _ _ _).
 Qed.
 
 Global Instance elim_modal_wp_sc_fence_rel (P : vProp Σ) tid E Φ p:
@@ -482,10 +478,9 @@ Proof.
   inv_head_step.
   lazymatch goal with [ X : lbl_machine_step _ _ _ _ _ _ _ _ _ |- _] =>
     inversion X end.
-  lazymatch goal with [ X : sc_fence_step _ _ _ _ |- _] =>
-    inversion X end.
-  lazymatch goal with [ X : sc_fence_helper _ _ _ _ |- _] =>
-    inversion X end. subst. simpl in *. solve_lat.
+  destruct select (sc_fence_step _ _ _ _).
+  destruct select (sc_fence_helper _ _ _ _).
+  subst. apply lat_join_sqsubseteq_l.
 Qed.
 
 Global Instance elim_modal_wp_sc_fence_acq (P : vProp Σ) tid E Φ p: