proposition: Lemma setXb_eq_gfunctions f x: (forall i, inc i (domain f) -> Vg f i = x) -> productb f = gfunctions (domain f) x.
proof: Proof. move=> prop; apply: extensionality. apply: setXb_sub_gfunctions =>//. by move=> y /setUb_P [z zd zV]; rewrite - (prop _ zd). move=> y /gfunctions_P2 [fy dy sr]; apply/setXb_P;split => // i id. rewrite (prop _ id); apply: sr; rewrite - dy in id; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)