proposition: Lemma empty_function_p2 f: function f -> target f = emptyset -> source f = emptyset.
proof: Proof. by move => ff te; apply /set0_P => x /(Vf_target ff); rewrite te => /in_set0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)