proposition: Lemma functions_empty X: functions emptyset X = singleton (empty_function_tg X).
proof: Proof. move: (empty_function_tg_function X) => h. apply: set1_pr; first by apply /functionsP. move: h => [fa sa ta]. move => z /functionsP [ft st tt]; apply: function_exten => //; try ue. by rewrite st => x /in_set0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)