proposition: Lemma empty_function_tg_function x: function_prop (empty_function_tg x) emptyset x.
proof: Proof. hnf; rewrite /empty_function_tg; aw; split => //; apply: function_pr; aww. apply: fgraph_set0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)