proposition: Lemma setXb_gi X f: (forall i, inc i (domain X) -> inc (f i) (Vg X i)) -> inc (Lg (domain X) f) (productb X).
proof: Proof. move => H; apply/setXb_P; split; aww. by move => i idx; rewrite LgV //; apply:H. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)