diff --git a/tests/lean/run/blast9.lean b/tests/lean/run/blast9.lean index 5b5c59e539..ee4e2370b7 100644 --- a/tests/lean/run/blast9.lean +++ b/tests/lean/run/blast9.lean @@ -5,6 +5,8 @@ set_option blast.strategy "preprocess" example (p : Prop) (a b c : nat) : [a, b, c] = [] → p := by blast +set_option blast.strategy "simple" + lemma l1 (a b c d e f : nat) : [a, b, c] = [d, e, f] → a = d ∧ b = e ∧ c = f := by blast