theory Test
imports Main
begin

declare [[simp_trace_new, ML_exception_debugger]]

lemma "(\<exists>x. P x) \<or> Q \<equiv> \<exists>x. P x \<or> Q"
  quickcheck [tester = random]
  oops

end