proposition: Lemma gfunctions_P2 a b z: inc z (gfunctions a b) <-> [/\ fgraph z, domain z = a & sub (range z) b].
proof: Proof. split; first by move/gfunctions_P1 => [pa pb] /corr_propcc [_ _ pc]. move => [pa pb pc]; apply/gfunctions_P1;split => //. apply/corr_propcc;rewrite pb;split; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)