theory Barf
imports Main
begin

  definition graph :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('a \<times> 'b) set"
  where "graph A B f = {(a, b). a \<in> A \<and> b \<in> B \<and> f a = b}"

  lemma "graph A B f \<subseteq> (graph A B f) O (Id_on B)"
    using graph_def
    (* try
         "cvc4": Try this: by auto (37 ms).
         "z3": Try this: by auto (53 ms).
     *)
    by auto
    (* Failed to finish proof\<here>:
       goal (1 subgoal):
        1. \<And>a b. (\<And>A B f. graph A B f = {(a, b). a \<in> A \<and> b \<in> B \<and> f a = b}) \<Longrightarrow>
                  (a, b) \<in> graph A B f \<Longrightarrow> (a, b) \<in> graph A B f O Id_on B
     *)

end