proposition: Lemma disjointU_function_pr f: function (disjointU_function f) /\ graph (disjointU_function f) = (disjointU_fam f).
proof: Proof. rewrite /disjointU_function /disjointU_fam. by split; [ apply: function_pr; [ fprops | fprops | aw] | aw ]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)