theory Scratch
  imports Main
begin

lemma
  assumes "\<And>a . \<exists>!x. f x = [a]"
  shows "\<exists>!x. \<exists>!y. f x = [a] \<and> f y = [b]"
proof  -
  have ?thesis
    using assms by smt (* exception Option raised (line 82 of "General/basics.ML") *)
  show ?thesis
    using assms by metis (* works *)
qed

end