proposition: Lemma setXb_monotone2 f g: domain f = domain g -> nonempty_fam f -> sub (productb f) (productb g) -> (forall i, inc i (domain f) -> sub (Vg f i) (Vg g i)).
proof: Proof. move=> dfdg alne sfg i id j jV. have jt: (inc j (target (pr_i f i))) by rewrite/ pr_i; aw. move:((proj2 (pri_fs alne id)) _ jt) => [x xs ->]. move: xs; rewrite /pr_i lf_source=>xs. rewrite pri_V //. by move /setXb_P: (sfg _ xs) => [fx dx]; apply; rewrite -dfdg. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)