proposition: Lemma function_pr s t g: fgraph g -> sub (range g) t -> s = domain g -> function (triple s t g).
proof: Proof. rewrite /function => fg sr d; aw; split => //. by apply: corresp_create; rewrite d; apply /corr_propcc; split => //;case: fg. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)