adapt for coq/coq#17022 (#96)

mit-plv · Feb 15, 2023 · 77c76a4 · 77c76a4
1 parent c26f81b
commit 77c76a4
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/src/Rewriter/Util/ListUtil.v b/src/Rewriter/Util/ListUtil.v
@@ -542,8 +542,8 @@ Lemma list_bl_hetero {A B} {AB_beq : A -> B -> bool} {AB_R : A -> B -> Prop}
   : forall {x y},
     list_beq_hetero AB_beq x y = true -> list_eq AB_R x y.
 Proof using Type.
-  induction x, y; cbn in *; eauto; try congruence.
-  rewrite Bool.andb_true_iff; intuition eauto.
+  induction x, y; cbn in *; eauto; try congruence;
+  try (rewrite Bool.andb_true_iff; intuition eauto).
 Qed.
 
 Lemma list_lb_hetero {A B} {AB_beq : A -> B -> bool} {AB_R : A -> B -> Prop}