proposition: Lemma setXb_ne f: nonempty_fam f -> nonempty (productb f).
proof: Proof. move=> hyp. exists (Lg (domain f)(fun i=> rep (Vg f i))). by apply:setXb_gi => i /hyp/rep_i. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)