proposition: Lemma empty_source_graph2 f: function f -> source f = emptyset -> f = empty_function_tg (target f).
proof: Proof. move => pa pb;have pc:= (empty_source_graph pa pb). by rewrite /empty_function_tg -{1} (corresp_recov (proj1 (proj31 pa))) pb pc. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)