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