diff --git a/iris/program_logic/ectx_language.v b/iris/program_logic/ectx_language.v
index a4c2e0c07b09890341052d7c90e9911c977c39df..a30b5a7d6edc7833cf2d26cccf4d245f7bee0f65 100644
--- a/iris/program_logic/ectx_language.v
+++ b/iris/program_logic/ectx_language.v
@@ -310,6 +310,7 @@ Section ectx_language.
 End ectx_language.
 
 Global Arguments ectx_lang : clear implicits.
+Global Arguments Ectx_step {Λ e1 σ1 κ e2 σ2 efs}.
 Coercion ectx_lang : ectxLanguage >-> language.
 
 (* This definition makes sure that the fields of the [language] record do not
diff --git a/iris/program_logic/total_adequacy.v b/iris/program_logic/total_adequacy.v
index 60cddc202320fc9900be272eb4cd1230ca36b36d..1e95546808a97793757eaef272dbe93bc9cba3a8 100644
--- a/iris/program_logic/total_adequacy.v
+++ b/iris/program_logic/total_adequacy.v
@@ -67,7 +67,7 @@ Proof.
   apply app_eq_inv in Ht as [(t&?&?)|(t&?&?)]; subst.
   - destruct t as [|e1' ?]; simplify_eq/=.
     + iMod ("IH2" with "[%] Hσ1") as (n2) "($ & Hσ & IH2 & _)".
-      { by eapply step_atomic with (t1:=[]). }
+      { by eapply (step_atomic _ _ _ _ _ _ _ _ []). }
       iModIntro. iExists n2. iFrame "Hσ".
       rewrite -{2}(left_id_L [] (++) (e2 :: _)). iApply "IH2".
       by setoid_rewrite (right_id_L [] (++)).
diff --git a/iris/proofmode/coq_tactics.v b/iris/proofmode/coq_tactics.v
index 81d01599e8b079d0599ffc7250a97096518be1d8..3be114662a8f95836da8e865485ab0d87915dc3b 100644
--- a/iris/proofmode/coq_tactics.v
+++ b/iris/proofmode/coq_tactics.v
@@ -1048,7 +1048,7 @@ Section tac_modal_intro.
         naive_solver. }
     assert (□ [∧] Γp ⊢ M (□ [∧] Γp'))%I as HMp.
     { remember (modality_intuitionistic_action M).
-      destruct HΓp as [?|M C Γp ?%TCForall_Forall|? M C Γp Γp' []|? M Γp|M Γp]; simpl.
+      destruct HΓp as [? M|M C Γp ?%TCForall_Forall|? M C Γp Γp' []|? M Γp|M Γp]; simpl.
       - rewrite {1}intuitionistically_elim_emp (modality_emp M)
           intuitionistically_True_emp //.
       - eauto using modality_intuitionistic_forall_big_and.
@@ -1059,7 +1059,7 @@ Section tac_modal_intro.
       - eauto using modality_intuitionistic_id. }
     move: HQ'; rewrite -HQ pure_True // left_id HMp=> HQ' {HQ Hwf HMp}.
     remember (modality_spatial_action M).
-    destruct HΓs as [?|M C Γs ?%TCForall_Forall|? M C Γs Γs' fi []|? M Γs|M Γs]; simpl.
+    destruct HΓs as [? M|M C Γs ?%TCForall_Forall|? M C Γs Γs' fi []|? M Γs|M Γs]; simpl.
     - by rewrite -HQ' /= !right_id.
     - rewrite -HQ' {1}(modality_spatial_forall_big_sep _ _ Γs) //.
       by rewrite modality_sep.
diff --git a/iris_heap_lang/adequacy.v b/iris_heap_lang/adequacy.v
index 9dfd10fed77d7331312c014b3da82351beb523f0..d24fe5afd688caed7823936c38c27243e1faec04 100644
--- a/iris_heap_lang/adequacy.v
+++ b/iris_heap_lang/adequacy.v
@@ -20,7 +20,7 @@ Definition heap_adequacy Σ `{!heapPreG Σ} s e σ φ :
   (∀ `{!heapG Σ}, ⊢ inv_heap_inv -∗ WP e @ s; ⊤ {{ v, ⌜φ v⌝ }}) →
   adequate s e σ (λ v _, φ v).
 Proof.
-  intros Hwp; eapply (wp_adequacy _ _); iIntros (??) "".
+  intros Hwp; eapply (wp_adequacy _ _); iIntros (? κs) "".
   iMod (gen_heap_init σ.(heap)) as (?) "[Hh _]".
   iMod (inv_heap_init loc (option val)) as (?) ">Hi".
   iMod (proph_map_init κs σ.(used_proph_id)) as (?) "Hp".
diff --git a/iris_heap_lang/class_instances.v b/iris_heap_lang/class_instances.v
index 3d5682b82909b503d79ef55b96e60e4fcd80ebae..0e1f94c5a9fea9cdfb778c20ca2a2f5db84ac751 100644
--- a/iris_heap_lang/class_instances.v
+++ b/iris_heap_lang/class_instances.v
@@ -64,18 +64,18 @@ Section atomic.
   Proof.
     rename e into e1. intros H σ1 e2 κ σ2 efs [Ks e1' e2' Hfill -> step].
     simpl in *. induction Ks as [|K Ks _] using rev_ind; simpl in Hfill.
-    - subst. inversion_clear step. by apply (H σ1 (Val v) κs σ2 efs), head_prim_step.
+    - subst. inversion_clear step. by eapply (H σ1 (Val _) _ σ2 efs), head_prim_step.
     - rewrite fill_app. rewrite fill_app in Hfill.
       assert (∀ v, Val v = fill Ks e1' → False) as fill_absurd.
       { intros v Hv. assert (to_val (fill Ks e1') = Some v) as Htv by by rewrite -Hv.
         apply to_val_fill_some in Htv. destruct Htv as [-> ->]. inversion step. }
       destruct K; (inversion Hfill; clear Hfill; subst; try
         match goal with | H : Val ?v = fill Ks e1' |- _ => by apply fill_absurd in H end).
-      refine (_ (H σ1 (fill (Ks ++ [K]) e2') _ σ2 efs _)).
+      refine (_ (H σ1 (fill (Ks ++ [_]) e2') _ σ2 efs _)).
       + destruct s; intro Hs; simpl in *.
         * destruct Hs as [v Hs]. apply to_val_fill_some in Hs. by destruct Hs, Ks.
         * apply irreducible_resolve. by rewrite fill_app in Hs.
-      + econstructor 1 with (K := Ks ++ [K]); try done. simpl. by rewrite fill_app.
+      + econstructor; try done. simpl. by rewrite fill_app.
   Qed.
 End atomic.
 
diff --git a/iris_heap_lang/lang.v b/iris_heap_lang/lang.v
index 4705694be26e5bfa2e5564676a5e09367198bea8..bb686c72bbabec9c44fc49ff9cc1287d1281c9c5 100644
--- a/iris_heap_lang/lang.v
+++ b/iris_heap_lang/lang.v
@@ -797,5 +797,5 @@ Proof.
         apply to_val_fill_some in HEq; destruct HEq as [-> ->]; inversion step
       end).
     eapply (H κs (fill_item _ (foldl (flip fill_item) e2' Ks)) σ' efs).
-    eapply (Ectx_step _ _ _ _ _ _ (Ks ++ [_])); last done; simpl; by rewrite fill_app.
+    eapply (Ectx_step (Ks ++ [_])); last done; simpl; by rewrite fill_app.
 Qed.
diff --git a/iris_heap_lang/primitive_laws.v b/iris_heap_lang/primitive_laws.v
index 271eaa855a22d453da2b5425b8f099bdf82ecbfc..236c1d0227109411df8953c982d072ab43e7270a 100644
--- a/iris_heap_lang/primitive_laws.v
+++ b/iris_heap_lang/primitive_laws.v
@@ -224,7 +224,7 @@ Proof.
   iIntros (Hn Φ) "_ HΦ". iApply twp_lift_atomic_head_step_no_fork; first done.
   iIntros (σ1 κs k) "[Hσ Hκs] !>"; iSplit; first by destruct n; auto with lia head_step.
   iIntros (κ v2 σ2 efs Hstep); inv_head_step.
-  iMod (gen_heap_alloc_big _ (heap_array l (replicate (Z.to_nat n) v)) with "Hσ")
+  iMod (gen_heap_alloc_big _ (heap_array _ (replicate (Z.to_nat n) v)) with "Hσ")
     as "(Hσ & Hl & Hm)".
   { apply heap_array_map_disjoint.
     rewrite replicate_length Z2Nat.id; auto with lia. }
@@ -380,6 +380,7 @@ Proof.
   iIntros (Φ) "_ HΦ". iApply wp_lift_atomic_head_step_no_fork; first done.
   iIntros (σ1 κ κs n) "[Hσ HR] !>". iSplit; first by eauto with head_step.
   iIntros "!>" (v2 σ2 efs Hstep). inv_head_step.
+  rename select proph_id into p.
   iMod (proph_map_new_proph p with "HR") as "[HR Hp]"; first done.
   iModIntro; iSplit; first done. iFrame. by iApply "HΦ".
 Qed.
@@ -393,7 +394,7 @@ Lemma resolve_reducible e σ (p : proph_id) v :
 Proof.
   intros A (κ & e' & σ' & efs & H).
   exists (κ ++ [(p, (default v (to_val e'), v))]), e', σ', efs.
-  eapply Ectx_step with (K:=[]); try done.
+  eapply (Ectx_step []); try done.
   assert (∃w, Val w = e') as [w <-].
   { unfold Atomic in A. apply (A σ e' κ σ' efs) in H. unfold is_Some in H.
     destruct H as [w H]. exists w. simpl in H. by apply (of_to_val _ _ H). }
@@ -409,18 +410,21 @@ Proof.
   induction Ks as [|K Ks _] using rev_ind.
   + simpl in *. subst. inv_head_step. by constructor.
   + rewrite fill_app /= in Hfill. destruct K; inversion Hfill; subst; clear Hfill.
-    - assert (fill_item K (fill Ks e1') = fill (Ks ++ [K]) e1') as Eq1;
+    - rename select ectx_item into Ki.
+      assert (fill_item Ki (fill Ks e1') = fill (Ks ++ [Ki]) e1') as Eq1;
         first by rewrite fill_app.
-      assert (fill_item K (fill Ks e2') = fill (Ks ++ [K]) e2') as Eq2;
+      assert (fill_item Ki (fill Ks e2') = fill (Ks ++ [Ki]) e2') as Eq2;
         first by rewrite fill_app.
       rewrite fill_app /=. rewrite Eq1 in A.
-      assert (is_Some (to_val (fill (Ks ++ [K]) e2'))) as H.
-      { apply (A σ1 _ κ σ2 efs). eapply Ectx_step with (K0 := Ks ++ [K]); done. }
+      assert (is_Some (to_val (fill (Ks ++ [Ki]) e2'))) as H.
+      { apply (A σ1 _ κ σ2 efs). eapply (Ectx_step (Ks ++ [Ki])); done. }
       destruct H as [v H]. apply to_val_fill_some in H. by destruct H, Ks.
-    - assert (to_val (fill Ks e1') = Some vp); first by rewrite -H1 //.
-      apply to_val_fill_some in H as [-> ->]. inv_head_step.
-    - assert (to_val (fill Ks e1') = Some vt); first by rewrite -H2 //.
-      apply to_val_fill_some in H as [-> ->]. inv_head_step.
+    - rename select (of_val vp = _) into Hvp.
+      assert (to_val (fill Ks e1') = Some vp) as Hfillvp by rewrite -Hvp //.
+      apply to_val_fill_some in Hfillvp as [-> ->]. inv_head_step.
+    - rename select (of_val vt = _) into Hvt.
+      assert (to_val (fill Ks e1') = Some vt) as Hfillvt by rewrite -Hvt //.
+      apply to_val_fill_some in Hfillvt as [-> ->]. inv_head_step.
 Qed.
 
 Lemma wp_resolve s E e Φ (p : proph_id) v (pvs : list (val * val)) :
diff --git a/iris_heap_lang/proph_erasure.v b/iris_heap_lang/proph_erasure.v
index 750b55bd4a852230ce59d89eb47a2c8fe6cfc6da..704a56c576dd7746c8795983f8ab400bba6065eb 100644
--- a/iris_heap_lang/proph_erasure.v
+++ b/iris_heap_lang/proph_erasure.v
@@ -420,7 +420,8 @@ Proof.
     eapply Resolve_3_vals_head_stuck; eauto. }
   rewrite fill_app in Hrs.
   destruct Ki; simplify_eq/=.
-  - pose proof (fill_item_val Ki (fill K e1')) as Hnv.
+  - rename select ectx_item into Ki.
+    pose proof (fill_item_val Ki (fill K e1')) as Hnv.
     apply fill_val in Hnv as [? Hnv]; last by rewrite -Hrs; eauto.
     by erewrite val_head_stuck in Hnv.
   - edestruct Hvfill as [? Heq]; eauto.
@@ -629,7 +630,7 @@ Proof.
   rewrite app_length in IHm; simpl in *.
   rewrite fill_app /=; rewrite fill_app /= in He1.
   eapply prim_step_matched_by_erased_steps_ectx_item; eauto; [].
-  { intros; simpl in *; apply (IHm (length K')); auto with lia. }
+  { intros K' **; simpl in *. apply (IHm (length K')); auto with lia. }
 Qed.
 
 Lemma head_step_erased_prim_step_CmpXchg v1 v2 σ l vl: