proposition: Lemma gfunctions_empty X: (gfunctions emptyset X) = \1c.
proof: Proof. apply: set1_pr. apply/gfunctions_P2; saw; fprops; apply fgraph_set0. by move => z /gfunctions_P2 [_ /domain_set0_P]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)