theory Foo
imports Complex_Main
begin

consts 
  F :: "('a \<Rightarrow> 'a) \<Rightarrow> 'c"

definition "g x = x"

lemma F_g: "F (\<lambda>x::'a. f (g x)) = F (\<lambda>x::'a. f x)"
  by (simp add: g_def)

notepad
begin
  have "F (\<lambda>x::'a. g x) = F (\<lambda>x::'a. x)"
    (* apply (simp only: F_g)  <- does not work *)
    apply (subst F_g, rule refl) (* <- works *)
    done
end

end