An exact proof term for the current goal is (functional_graph_graph X (λx0 : set ⇒ apply_fun g (apply_fun f x0))).