Skip to content

Commit 3dd62f8

Browse files
authored
1 parent b27e806 commit 3dd62f8

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

theories/Data/Fin.v

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -100,7 +100,7 @@ Proof.
100100
intro. destruct (fin_case y) ; subst.
101101
intuition.
102102
destruct H ; subst.
103-
intuition ; try congruence.
103+
intuition; auto with *; try congruence.
104104
(* inversion H.*)
105105
intro ; destruct (fin_case y) ; subst ; simpl.
106106
intuition ; try congruence.

0 commit comments

Comments
 (0)