proposition: Lemma p1graph_source1 x: inc x (graph f) -> inc (P x) (source f).
proof: Proof. move=> xgf; apply: (p1graph_source (y:= (Vf f (P x)))). by rewrite - (in_graph_Vf xgf). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)