Fix anomaly

mit-plv · Aug 3, 2023 · 44b0f8f · 44b0f8f
1 parent 8e0c039
commit 44b0f8f
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/PyLevelLang/src/PyLevelLang/SamplePrograms.v b/PyLevelLang/src/PyLevelLang/SamplePrograms.v
@@ -573,7 +573,7 @@ Section WithMap.
     intros.
     inversion H; subst.
     rewrite H2; try easy.
-    firstorder idtac.
+    eapply IHl; eauto.
   Qed.
 
   Lemma fold_left_no_ans (l : list Z) m :