proposition: Lemma fun_set_to_prod1 F f i: fgraph F -> inc i (domain F) -> function f -> target f = productb F -> function_prop (pr_i F i \co f) (source f) (Vg F i) /\ (forall x, inc x (source f) -> Vf (pr_i F i \co f) x = Vg (Vf f x) i).
proof: Proof. move=> fF id ff tfpF. have aux: (pr_i F i) \coP f. split => //; [by apply: pri_f=>// | by symmetry; rewrite /pr_i; aw]. rewrite /function_prop {2 3} /pr_i; aw; split. by saw; fct_tac. move=> x xs; rewrite compfV //; rewrite pri_V //; rewrite -tfpF; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)