theory Barf
imports Main
begin

  definition graph :: "'a set \<Rightarrow> 'a set \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
  (*
   * With the more general type "'a set \<Rightarrow> ' b set \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool"
   * the proof by fastforce succeeds below.
   *)
  where "graph A B f a b = (a \<in> A \<and> b \<in> B \<and> f a = b)"

  lemma "a \<in> A \<and> b \<in> B \<and> c \<in> C \<and> f a = b \<and> g b = c \<Longrightarrow> graph A C (g o f) a c"
    using graph_def
    (* try0 (* Says: 'Try this: by fastforce' *) *)
    by fastforce  (* Fails to prove lemma -- unification bound exceeded, etc. *)

end