proposition: Lemma Eq_src_graph f: function f -> (source f) \Eq (graph f).
proof: Proof. move=> ff. apply: (@equipotent_aux (fun z => J z (Vf f z)));apply: lf_bijective. - move=> z jz /=;Wtac. - move=> u v _ _ aux; exact: (pr1_def aux). - move=> y yG; move: (p1graph_source1 ff yG) => pa; ex_tac. apply: in_graph_V => //; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)