proposition: Lemma fun_set_to_prod2 f gf: inc gf (gfunctions src (productb F)) -> f = (triple src (productb F) gf) -> function_prop f src (productb F).
proof: Proof. move=> igf eq. have [g [fg sg tg gg]] := (gfunctions_hi igf). have -> // : f = g. by rewrite eq - sg -tg -gg; apply: corresp_recov1; move: fg=> [ res _]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)