proposition: Theorem distrib_union_inter f: (forall l, inc l (domain f) -> nonempty (domain (Vg f l))) -> unionf (domain f) (fun l => intersectionb (Vg f l)) = intersectionf (productf (domain f) (fun l => (domain (Vg f l)))) (fun g => (unionf (domain f) (fun l => Vg (Vg f l) (Vg g l)))).
proof: Proof. move=> alne; set_extens s => xu. apply: setIf_i. by apply: setXb_ne; fprops; hnf; aw => i id; rewrite LgV //; apply: alne. move /setUf_P: xu => [y yf si] j /setXf_P [fgj dj]; aw => aa. move: (aa _ yf); aw => bb; move: (setIb_hi si bb) => cc; union_tac. ex_middle nsu. set gl:= (fun l => Zo (domain (Vg f l)) (fun i => ~ (inc s (Vg (Vg f l) i)))). have ne: (nonempty (productf (domain f) gl)). apply: setXb_ne; fprops; hnf; aw=> i id; rewrite LgV // /gl; set jl:=Zo _ _ . case: (emptyset_dichot jl) =>// je; case: nsu; union_tac. apply: setIb_i; [by apply /domain_set0P; apply: alne | ]. by move=> j jd; ex_middle hyp; empty_tac1 j; apply: Zo_i. move: ne=> [y] /setXf_P [fy dy iVz]. have yp: inc y (productf (domain f) (fun l => domain (Vg f l))). apply/setXf_P; split =>// i id. by case /Zo_P: (iVz _ id). by move /setUf_P: (setIf_hi xu yp) => [z zdf sv]; case/Zo_P: (iVz _ zdf). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)