diff --git a/erasure/theories/EConstructorsAsBlocks.v b/erasure/theories/EConstructorsAsBlocks.v
index 87f53f5143..319f02fd7c 100644
--- a/erasure/theories/EConstructorsAsBlocks.v
+++ b/erasure/theories/EConstructorsAsBlocks.v
@@ -103,7 +103,7 @@ Section transform_blocks.
   Qed.
 
   Lemma chop_eq {A} n (l : list A) l1 l2 : chop n l = (l1, l2) -> l = l1 ++ l2.
-  Proof.
+  Proof using Type.
     rewrite chop_firstn_skipn. intros [= <- <-].
     now rewrite firstn_skipn.
   Qed.
@@ -188,7 +188,7 @@ Section transform_blocks.
       | view_other fn nconstr =>
           mkApps (transform_blocks fn) (map transform_blocks args)
       end.
-  Proof.
+  Proof using Type.
     destruct (decompose_app f) eqn:da.
     rewrite (decompose_app_inv da). rewrite transform_blocks_mkApps.
     now eapply decompose_app_notApp.
@@ -210,7 +210,7 @@ Section transform_blocks.
         P (mkApps (transform_blocks fn) (map transform_blocks args))
     end) ->
     P (transform_blocks (mkApps fn args)).
-  Proof.
+  Proof using Type.
     intros napp.
     move/isEtaExp_mkApps.
     rewrite decompose_app_mkApps //.
@@ -228,7 +228,7 @@ Section transform_blocks.
 
   Lemma transform_blocks_mkApps_eta_fn f args : isEtaExp Σ f ->
     transform_blocks (mkApps f args) = mkApps (transform_blocks f) (map (transform_blocks) args).
-  Proof.
+  Proof using Type.
     intros ef.
     destruct (decompose_app f) eqn:df.
     rewrite (decompose_app_inv df) in ef |- *.
@@ -1147,6 +1147,9 @@ Proof.
     destruct nth_error; try now inv Heq.
     destruct nth_error; invs Heq.
     rewrite /wf_minductive in E. rtoProp.
+    let H4' := match goal with H : context[has_cstr_params] |- _ => H end in
+    rename H4 into H4_old;
+    rename H4' into H4.
     rewrite haspars /= in H4.
     cbn in H4. eapply eqb_eq in H4.
     unfold cstr_arity in H0.
@@ -1154,6 +1157,8 @@ Proof.
     revert E1 E2.
     rewrite <- H0.
     rewrite !chop_firstn_skipn !firstn_all. intros [= <- <-] [= <- <-].
+    let X0' := match goal with H : All2 _ _ _ |- _ => H end in
+    rename X0' into X0.
     eapply All2_length in X0 as Hlen.
     cbn.
     rewrite !skipn_all Hlen skipn_all firstn_all. cbn.
diff --git a/erasure/theories/EEtaExpanded.v b/erasure/theories/EEtaExpanded.v
index beffd79041..90415ebc3c 100644
--- a/erasure/theories/EEtaExpanded.v
+++ b/erasure/theories/EEtaExpanded.v
@@ -662,6 +662,7 @@ Proof.
   destruct (isConstruct f) eqn:eqc.
   destruct f => //.
   - depelim H; try solve_discr_args => //.
+    let H3 := match goal with H : tConstruct _ _ _ = tConstruct _ _ _ |- _ => H end in
     noconf H3.
     eapply expanded_tConstruct_app; tea. cbn in H0. lia. solve_all.
   - destruct args using rev_ind; cbn => //.
diff --git a/erasure/theories/EEtaExpandedFix.v b/erasure/theories/EEtaExpandedFix.v
index 08ae9e1b97..57656b29b3 100644
--- a/erasure/theories/EEtaExpandedFix.v
+++ b/erasure/theories/EEtaExpandedFix.v
@@ -1570,7 +1570,7 @@ Lemma eval_app_cong_tApp' fl Σ t arg arg' res :
   @eval (switch_unguarded_fix fl) Σ (tApp t arg') res ->
   @eval (switch_unguarded_fix fl) Σ (tApp t arg) res.
 Proof.
-  intros. depind H0.
+  intros X H H0. depind H0.
   - eapply eval_app_cong_tApp; tea. econstructor. constructor. constructor. exact H.
   - pose proof (eval_trans' H H0_0). subst a'. econstructor; tea.
   - pose proof (eval_trans' H H0_0). subst av. eapply eval_fix; tea.
@@ -1612,7 +1612,7 @@ Lemma eval_app_cong_mkApps {fl} {Σ} {f f' res : EAst.term} {args args'} :
   @eval (switch_unguarded_fix fl) Σ (mkApps f args) res.
 Proof.
   revert args' res; induction args using rev_ind.
-  - cbn. intros. eapply eval_trans. tea. now depelim X.
+  - cbn. intros args' res ? X ?. eapply eval_trans. tea. now depelim X.
   - intros args' res evf evargs evf'.
     rewrite !mkApps_app. cbn.
     eapply All2_app_inv_l in evargs as [r1 [r2 [? []]]]. depelim a0. depelim a0. subst args'.
@@ -1737,7 +1737,7 @@ Proof.
       rewrite -[tApp _ _](mkApps_app _ _ [av]) in IHeval3.
       forward_keep IHeval2.
       { rewrite ha. now eapply forallb_last. }
-      unshelve epose proof (eval_mkApps_tFix_inv_size _ _ _ _ _ _ H') => //; auto.
+      unshelve epose proof (eval_mkApps_tFix_inv_size _ _ _ _ _ _ H') as X => //; auto.
       intros hev.
       destruct X as [[args' [hargs heq]]|].
       { solve_discr. noconf H5.
diff --git a/erasure/theories/EWcbvEval.v b/erasure/theories/EWcbvEval.v
index 8289ab60a6..75ee2581af 100644
--- a/erasure/theories/EWcbvEval.v
+++ b/erasure/theories/EWcbvEval.v
@@ -899,7 +899,7 @@ Section Wcbv.
 
   Lemma value_app_inv L : value (mkApps tBox L) -> L = nil.
   Proof.
-    intros. depelim X.
+    intro X. depelim X.
     - destruct L using rev_ind.
       reflexivity.
       rewrite mkApps_app in i. inv i.
@@ -1059,7 +1059,8 @@ Section Wcbv.
       { clear -X; induction X; constructor; auto. }
       econstructor; tea; auto.
     - assert (All2 eval args args).
-      { clear -X0; induction X0; constructor; auto. }
+      { let X0 := match goal with H : All (fun t => eval t t) _ |- _ => H end in
+        clear -X0; induction X0; constructor; auto. }
       eapply eval_mkApps_cong => //. now eapply value_head_final.
   Qed.
 
@@ -1294,7 +1295,7 @@ Section Wcbv.
     All2 eval t v' ->
     v = v'.
   Proof.
-    induction 1 in v' |- *; intros H; depelim H; auto. f_equal; eauto.
+    induction 1 in v' |- *; intros H'; depelim H'; auto. f_equal; eauto.
     now eapply eval_deterministic.
   Qed.
 
@@ -2037,9 +2038,9 @@ Lemma eval_box_apps {wfl : WcbvFlags}:
     eval Σ' e tBox -> eval Σ' (mkApps e x) tBox.
 Proof.
   intros Σ' e x H2.
-  revert e H2; induction x using rev_ind; cbn; intros; eauto.
+  revert e H2; induction x using rev_ind; cbn; intros e ? X ?; eauto.
   eapply All2_app_inv_l in X as (l1' & l2' & -> & H' & H2).
   depelim H2.
   specialize (IHx e _ H'). simpl.
   rewrite mkApps_app. simpl. econstructor; eauto.
-Qed.
\ No newline at end of file
+Qed.
diff --git a/erasure/theories/EWcbvEvalEtaInd.v b/erasure/theories/EWcbvEvalEtaInd.v
index a4e7eb32f4..a8e6e1ab35 100644
--- a/erasure/theories/EWcbvEvalEtaInd.v
+++ b/erasure/theories/EWcbvEvalEtaInd.v
@@ -765,7 +765,10 @@ Proof.
   all:intuition auto.
   - eapply eval_wellformed; tea => //.
   - rewrite isEtaExp_Constructor => //.
+    let X0 := multimatch goal with H : All2 _ _ _ |- _ => H end in
+    let H1 := multimatch goal with H : _ = _ |- _ => H end in
     rewrite -(All2_length X0) H1. cbn. rtoProp; intuition eauto.
+    match goal with H : ?f ?n |- ?f ?n' => replace n' with n by congruence; exact H end.
     cbn; eapply All_forallb. eapply All2_All_right; tea.
     cbn. intros x y []; auto.
 Qed.
diff --git a/erasure/theories/EWcbvEvalNamed.v b/erasure/theories/EWcbvEvalNamed.v
index 6d57c80cd4..f7bb1edc0b 100644
--- a/erasure/theories/EWcbvEvalNamed.v
+++ b/erasure/theories/EWcbvEvalNamed.v
@@ -1328,13 +1328,20 @@ Proof.
   revert HE Hsunny. pattern E, s, v, Heval.
   revert E s v Heval.
   eapply eval_ind; intros; eauto; cbn in *; rtoProp; eauto using Forall.
-  - do 2 forward X; eauto. inv X.
-    eapply X1; eauto. econstructor; cbn; eauto.
+  - let X := match reverse goal with H : All _ _ -> _ -> _ |- _ => H end in
+    do 2 forward X; eauto; inv X.
+    let X1 := multimatch goal with H : _ |- _ => H end in
+    now eapply X1; eauto; econstructor; cbn; eauto.
   - econstructor; eauto. unfold fresh in H. destruct in_dec; cbn in *; congruence.
-  - eapply X0. econstructor; cbn; eauto. eauto.
-  - solve_all. inv X.
+  - let X0 := multimatch goal with H : _ |- _ => H end in
+    now eapply X0; [ econstructor; cbn; eauto | eauto ].
+  - solve_all.
+    let X := match goal with H : wf (vConstruct _ _ _) |- _ => H end in
+    inv X.
+    let X0 := match goal with H : All _ _ -> _ -> _ |- _ => H end in
     eapply X0. eapply wf_add_multiple; eauto.
     len. eapply All2_length in f4. lia.
+    let H := match goal with H : All (fun x => is_true (_ && _ && _)) _ |- _ => H end in
     eapply All_nth_error in H. 2: eauto. rtoProp.
     solve_all.
     rewrite map_fst_add_multiple. len.
@@ -1344,15 +1351,18 @@ Proof.
                  | nNamed na => [na]
                  end) br.1) as -> by eauto.
     clear - f4. induction f4; cbn; f_equal; destruct r, x; cbn; congruence.
-  - do 2 forward X; eauto. invs X.
+  - let X := match goal with H : All _ _ -> _ -> wf (vRecClos _ _ _) |- _ => H end in
+    do 2 forward X; eauto; invs X.
+    let X0 := match goal with H : All _ (add _ _ _) -> _ -> wf _ |- _ => H end in
     eapply X0.
     + econstructor; cbn; eauto.
       eapply wf_add_multiple; eauto.
       now rewrite map_length fix_env_length.
       eapply wf_fix_env; eauto.
-    + eapply All_nth_error in X2; eauto. cbn in X2. rtoProp.
-      rewrite map_fst_add_multiple. now rewrite map_length fix_env_length.
-      eauto.
+    + let X2 := multimatch goal with H : All _ _ |- _ => H end in
+      eapply All_nth_error in X2; eauto; cbn in X2; rtoProp;
+      rewrite map_fst_add_multiple; first [ now rewrite map_length fix_env_length
+      | eauto ].
   - assert (map fst (MCList.map2 (λ (n : ident) (d0 : def term), (n, EAst.dbody d0)) nms mfix) = nms) as EE. {
     clear - f6. induction f6; cbn; f_equal; eauto. }
     econstructor.
@@ -1399,9 +1409,10 @@ Proof.
       destruct r as [[? []]].
       destruct x; cbn in *; subst; eauto.
    + eauto.
-  - eapply X; eauto. eapply declared_constant_Forall in isdecl.
+  - let X := match goal with H : All _ _ -> _ -> wf _ |- _ => H end in
+    eapply X; eauto. eapply declared_constant_Forall in isdecl.
     2: eapply Forall_impl. 2: eauto.
-    2: { cbn. intros [] ?. cbn in *.  exact H. }
+    2: { cbn. intros [] ?. cbn in *. let H := match goal with H : match _ with ConstantDecl _ => _ | _ => _ end |- _ => H end in exact H. }
     cbn in *. destruct decl; cbn in *.
     subst. eauto.
   - solve_all. econstructor.
@@ -1579,7 +1590,8 @@ Proof.
       edestruct s1 as (? & ? & ?); eauto.
       invs Hv1. eexists; split; eauto. econstructor; eauto.
   - invs Hrep.
-    + invs H3.
+    + let H3 := match goal with H : ⊩ _ ~ tApp _ _ |- _ => H end in
+      invs H3.
     + cbn in Hsunny. rtoProp.
       edestruct s0 as (v1 & Hv1 & Hv2). 3: eauto. eauto. eauto.
       invs Hv1.
@@ -1603,6 +1615,7 @@ Proof.
   - assert (pars = 0) as ->. {
       unfold constructor_isprop_pars_decl in *.
       destruct lookup_constructor as [[[[] [? ?]] ?] | ] eqn:EE; cbn in *; try congruence.
+      let H0 := match goal with H : Some _ = Some _ |- _ => H end in
       invs H0.
       destruct lookup_env eqn:EEE; try congruence.
       eapply lookup_env_wellformed in EEE; eauto.
@@ -1621,7 +1634,8 @@ Proof.
       eapply All2_Set_All2 in H14. eapply All2_nth_error_Some_right in H14 as He2. 2: eauto.
       destruct He2 as (br' & Hnth & nms & Hbrs & Hbr & Hnodup). invs Hv1.
       edestruct s1 as (v2 & Hv1_ & Hv2_).
-      1: { eapply forallb_nth_error in H6. setoid_rewrite Hnth in H6. cbn in H6. rtoProp.
+      1: { let H6 := match goal with H : is_true (forallb _ _) |- _ => H end in
+        eapply forallb_nth_error in H6; setoid_rewrite Hnth in H6; cbn in H6. rtoProp.
            assert (nms = flat_map (λ x : name, match x with
                | nAnon => []
                | nNamed na => [na]
@@ -1630,6 +1644,9 @@ Proof.
            { rewrite Heqnms flat_map_concat_map.
              intros ? (? & ([] & <- & ?) % in_map_iff & Hd) % in_concat; cbn in *; eauto.
             destruct Hd; subst; eauto.
+            let H6' := match goal with H : is_true (forallb _ _) |- _ => H end in
+            rename H6 into H6_old;
+            rename H6' into H6.
             eapply forallb_forall in H6; eauto.
             cbn in H6. unfold fresh in H6. destruct in_dec; cbn in *; congruence. }
             { subst. unfold dupfree in H9. destruct dupfree_dec_ident; cbn in *; congruence. }
@@ -1647,7 +1664,10 @@ Proof.
            eapply All2_Set_All2, All2_length in H10; eauto.
            eapply All2_Set_All2, All2_length in Hbrs; eauto.
            rewrite -> !skipn_length in *. lia.
-        -- eapply forallb_nth_error in H6. setoid_rewrite Hnth in H6. cbn in H6. rtoProp.
+        -- let H6' := match goal with H : is_true (forallb _ _) |- _ => H end in
+           rename H6 into H6_old;
+           rename H6' into H6.
+           eapply forallb_nth_error in H6. setoid_rewrite Hnth in H6. cbn in H6. rtoProp.
            enough (nms = flat_map (λ x : name, match x with
            | nAnon => []
            | nNamed na => [na]
@@ -1669,9 +1689,9 @@ Proof.
         rewrite -> !skipn_length in *. lia.
       * solve_all.
       * now rewrite rev_involutive in Hv2_.
-  - eapply X; eauto. (* artifact of the induction being weird and having a trivial assumption to not mess up proof script. FIXME! *)
+  - eauto. (* artifact of the induction being weird and having a trivial assumption to not mess up proof script. FIXME! *)
   - invs Hrep.
-    + invs H5. invs H6.
+    + invs H5.
     + cbn -[substl] in *. rtoProp.
       edestruct s0 as (v & IH1 & IH2). 3, 1, 2: eauto.
       invs IH1.
@@ -1687,6 +1707,10 @@ Proof.
       eapply eval_wf in IH2 as Hwf; eauto.
       invs Hwf.
 
+      let H12 := match goal with H : NoDup (map fst vfix) |- _ => H end in
+      let H16 := match goal with H : forall nm, In nm (map fst vfix) -> ~In nm _ |- _ => H end in
+      let X := match goal with H : All (fun t => is_true (sunny _ _)) vfix |- _ => H end in
+      let X0 := match goal with H : All (fun v => wf _) _ |- _ => H end in
       rename H12 into dupfree_vfix, H16 into distinct_vfix_E0, X into sunny_in_vfix, X0 into wf_E0.
 
       edestruct s2 as (v'' & IH1'' & IH2'').
@@ -1706,7 +1730,7 @@ Proof.
       }
       { intros ? [-> | ?].
         - eapply All_nth_error in sunny_in_vfix; eauto.
-          cbn in sunny_in_vfix. rtoProp. unfold fresh in H2.
+          cbn in sunny_in_vfix. rtoProp. unfold fresh in *.
           destruct in_dec; cbn in *; eauto.
           rewrite in_app_iff in n. eauto.
         - eapply distinct_vfix_E0; eauto.
@@ -1776,7 +1800,8 @@ Proof.
       edestruct s0 as (v & Hv1 & Hv2). 1: eauto. eauto. econstructor.
       eexists. split. eauto. econstructor; eauto.
   - invs Hrep.
-    + invs H2.
+    + let H2 := multimatch goal with H : _ |- _ => H end in
+      now invs H2.
     + cbn in Hsunny. rtoProp.
       eapply eval_to_value in ev as Hval. invs Hval.
       * destruct f'; cbn in *; try congruence.
@@ -1786,19 +1811,30 @@ Proof.
         invs Hv1; destruct args using rev_ind; cbn in *; try congruence.
         all: match goal with [H : _ = mkApps _ _ |- _ ] => now rewrite mkApps_app in H end.
   - invs Hrep.
-    + invs H2. eexists. split. econstructor.  instantiate (1 := vs).
-      * eapply All2_All2_Set. eapply All2_Set_All2 in H5.
-        eapply All2_All2_mix in X. 2: eapply X0.
-        solve_all. eapply All2_trans'. 2: eauto. 2: exact X.
-        intros. destruct X1, p, a. eapply eval_represents_value; eauto.
+    + let H2 := match goal with H : ⊩ _ ~ tConstruct _ _ _ |- _ => H end in
+      invs H2. eexists. split. econstructor.  instantiate (1 := vs).
+      * eapply All2_All2_Set.
+        let H5 := multimatch goal with H : _ |- _ => H end in
+        eapply All2_Set_All2 in H5.
+        let X := match goal with H : All2 (EWcbvEval.eval _) _ _ |- _ => H end in
+        eapply All2_All2_mix in X. 2: let X0 := match goal with H : All2 (fun _ _ => MCProd.and3 _ _ _) _ _ |- _ => H end in exact X0.
+        solve_all. eapply All2_trans'. 2: eauto. 2: let X := match goal with H : All2 (fun _ _ => _ * EWcbvEval.eval _ _ _) _ _ |- _ => H end in exact X.
+        intros x y z [? [? ?]]. eapply eval_represents_value; eauto.
       * econstructor. eauto.
     + cbn in Hsunny.
       solve_all.
+      let H5' := multimatch goal with H : _ |- _ => H end in
+      rename H5' into H5.
       eapply All2_Set_All2 in H5.
       eapply All2_All_mix_left in H5. 2: eauto.
+       let X' := match goal with H : All2 (EWcbvEval.eval _) _ _ |- _ => H end in
+       rename X into X_old;
+       rename X' into X.
+       let X0' := match goal with H : All2 (fun _ _ => MCProd.and3 _ _ _) _ _ |- _ => H end in
+       rename X0' into X0.
        eapply All2_All2_mix in X. 2: eapply X0.
        cbn in X. eapply All2_trans' in X. 3: eapply H5.
-       2:{ intros. destruct X1, p, p0, a.
+       2:{ intros x y z [[? r] [[s0] ?]].
            eapply s0 in r; eauto. exact r. }
        assert ({ vs & All3 (fun v x z => ⊩ v ~ z × eval Σ' E x v) vs args0 args'}) as [vs Hvs]. {
          clear - X. induction X. eexists; econstructor. destruct IHX as [vs Hvs].
diff --git a/erasure/theories/ErasureCorrectness.v b/erasure/theories/ErasureCorrectness.v
index 858b8bb883..5661f5a7a8 100644
--- a/erasure/theories/ErasureCorrectness.v
+++ b/erasure/theories/ErasureCorrectness.v
@@ -264,6 +264,7 @@ Proof.
       2:{
       exists x2. split; eauto. constructor. eapply eval_iota_sing => //.
       pose proof (Ee.eval_to_value _ _ He_v').
+      let X0 := match goal with H : Ee.value _ (EAst.mkApps _ _) |- _ => H end in
       eapply value_app_inv in X0. subst. eassumption.
       depelim H2.
       eapply isErasable_Propositional in X0; eauto.
@@ -417,7 +418,11 @@ Proof.
             eapply declared_constructor_from_gen in d.
             eapply (declared_constructor_assumption_context d).
             destruct s3 as [? [? [eqp _]]].
-            rewrite lenppars (firstn_app_left) // in eqp. congruence.
+            rewrite lenppars (firstn_app_left) // in eqp.
+            match goal with
+            | [ H : ?f (firstn ?n ?ls) ?p |- ?f (firstn ?n' ?ls) ?p ]
+              => replace n' with n; first [ exact H | congruence ]
+            end.
             move: wf_brs. now rewrite /wf_branches hctors => h; depelim h.
             rewrite -eq_npars. exact s1.
           - eapply All2_rev. cbn.
@@ -438,7 +443,7 @@ Proof.
          constructor.
          destruct x1 as [n br'].
          eapply eval_iota_sing => //.
-         pose proof (Ee.eval_to_value _ _ He_v').
+         pose proof (Ee.eval_to_value _ _ He_v') as X0.
          apply value_app_inv in X0; subst x0.
          apply He_v'.
          now rewrite -eq_npars.
@@ -509,7 +514,7 @@ Proof.
         eapply isErasable_Proof. constructor. eauto.
 
         eapply eval_proj_prop => //.
-        pose proof (Ee.eval_to_value _ _ Hty_vc').
+        pose proof (Ee.eval_to_value _ _ Hty_vc') as X0.
         eapply value_app_inv in X0. subst. eassumption.
         now rewrite -eqpars.
       * rename H3 into Hinf.
@@ -549,7 +554,7 @@ Proof.
           eassumption.
           eapply isErasable_Proof.
           constructor. eapply eval_proj_prop => //.
-          pose proof (Ee.eval_to_value _ _ Hty_vc').
+          pose proof (Ee.eval_to_value _ _ Hty_vc') as X0.
           eapply value_app_inv in X0. subst. eassumption.
           now rewrite -eqpars.
         -- eapply erases_deps_eval in Hty_vc'; [|now eauto].