proposition: Lemma setXf_P I f x: inc x (productf I f) <-> [/\ fgraph x, domain x = I & forall i, inc i I -> inc (Vg x i) (f i)].
proof: Proof. split. move/setXb_P; aw; move => [pa pb pc];split => //. by move => i iI; move: (pc _ iI); rewrite LgV. move => [pa pb pc]; apply/setXb_P;aw;split => //. by move => i iI; rewrite LgV //; apply: pc. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)