diff --git a/tests/lean/run/blast_cc_noconfusion.lean b/tests/lean/run/blast_cc_noconfusion.lean index 462dc49af3..0e8c51c740 100644 --- a/tests/lean/run/blast_cc_noconfusion.lean +++ b/tests/lean/run/blast_cc_noconfusion.lean @@ -1,6 +1,8 @@ import data.list open nat +set_option blast.strategy "cc" + constant f : nat → nat example (a b c d : nat) : f d = f b → succ a = f b → f d = succ c → a = c :=