Fix some naming

Author: JasonGross

erasure/theories/EWcbvEvalNamed.v

@@ -1327,11 +1327,17 @@ 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.
     eapply All_nth_error in H. 2: eauto. rtoProp.