proposition: Lemma graph_of_function_V x y f: inc f (sub_functions x y) -> Vf (graph_of_function x y) f = graph f.
proof: Proof. rewrite /graph_of_function=> fs; rewrite LfV //; apply: set_of_graphs_pr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)