proposition: Lemma fun_set_small_target x: small_set (functions x emptyset).
proof: Proof. move=> u v uf vf; apply: (function_exten5 uf vf). move /functionsP: uf => [fa _ ta]; move/functionsP: vf => [fb _ tb]. rewrite !empty_target_graph//. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)