proposition: Theorem distrib_prod_intersection f: (forall l, inc l (domain f) -> nonempty (domain (Vg f l))) -> productf (domain f) (fun l => intersectionb (Vg f l)) = intersectionf (productf (domain f) (fun l => (domain (Vg f l)))) (fun g => (productf (domain f) (fun l => Vg (Vg f l) (Vg g l)))).
proof: Proof. move=> alne. have nep:(nonempty (productb (Lg (domain f) (fun l => domain (Vg f l))))). by apply: setXb_ne; fprops;hnf; hnf; aw => i id;rewrite LgV//; apply: alne. set_extens x => xp. apply: (setIf_i nep) =>j /setXf_P [fj dj iVd]. move /setXf_P: xp=>[fx xd iVi];apply/setXf_P; split => // i id. move: (iVi _ id) => ivdi; apply: (setIb_hi ivdi (iVd _ id)). move: nep=> [u up]; move: (setIf_hi xp up) => /setXf_P [fx dx iVx]. apply/setXf_P; split => // i id; apply: setIb_i; [ | move=> j jd]. by apply/domain_set0P; apply: alne. have: (nonempty (productf (domain f) (fun l => (Zo (domain (Vg f l)) (fun jj => l = i -> jj = j))))). apply: setXb_ne; fprops; hnf; hnf;aw=> k kd; rewrite LgV //. case: (equal_or_not k i)=> ki; first by exists j; apply: Zo_i; ue. move: (alne _ kd) => [y yd]; exists y; apply: Zo_i=>//. move=> [y] /setXf_P [fy dy iV]; move: (iV _ id); move/Zo_P => [_ aux]. have yd: (inc y (productf (domain f) (fun l => domain (Vg f l)))). by apply /setXf_P; split => // k kdf; move /Zo_P: (iV _ kdf) =>[]. move/setXf_P: (setIf_hi xp yd) =>[_ _ rel]. by move: (rel _ id); rewrite aux. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)