proposition: Lemma empty_target_graph f: function f -> target f = emptyset -> graph f = emptyset.
proof: Proof. move => ff sfe; apply /set0_P => x xp. case: (@in_set0 (Vf f (P x))); Wtac; Wtac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)