diff --git a/tests/lean/run/blast_ematch10.lean b/tests/lean/run/blast_ematch10.lean index 65c213b65..61890f120 100644 --- a/tests/lean/run/blast_ematch10.lean +++ b/tests/lean/run/blast_ematch10.lean @@ -1,4 +1,9 @@ attribute iff [reducible] +set_option blast.subst false +set_option blast.simp false -example (p : nat → Prop) (a b c : nat) : p a → a = b → p b := +definition lemma1 (p : nat → Prop) (a b c : nat) : p a → a = b → p b := by blast + +set_option pp.beta true +print lemma1