Skip to content

Commit

Permalink
adapt for coq/coq#17022 (#96)
Browse files Browse the repository at this point in the history
  • Loading branch information
andres-erbsen authored Feb 15, 2023
1 parent c26f81b commit 77c76a4
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions src/Rewriter/Util/ListUtil.v
Original file line number Diff line number Diff line change
Expand Up @@ -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}
Expand Down

0 comments on commit 77c76a4

Please sign in to comment.