proposition: Theorem distrib_inter_union f: intersectionf (domain f) (fun l => unionb (Vg f l)) = unionf (productf (domain f) (fun l => (domain (Vg f l)))) (fun g => (intersectionf (domain f) (fun l => Vg (Vg f l) (Vg g l)))).
proof: Proof. set_extens x => xi; last first. move /setUf_P: xi => [y /setXf_P [_ dy Vd] xi1]. case: (emptyset_dichot (domain f)) => ne. by move: xi1; rewrite ne setIf_0 => /in_set0. apply: (setIf_i ne) => j jd; move: (setIf_hi xi1 jd)=> u; union_tac. pose prop j a := (inc a (domain (Vg f j)) /\ inc x (Vg (Vg f j) a)). pose yf j:= choose (prop j). have p1: (forall j, inc j (domain f) -> (prop j (yf j))). move=> j jd; apply: choose_pr; move /setUb_P:(setIf_hi xi jd). by move => [y y1 y2];exists y; split. apply: (@setUf_i _ (Lg (domain f) yf)). by apply/setXf_P; split;aww=> i id; rewrite LgV//; move: (p1 _ id)=>[]. case: (emptyset_dichot (domain f)) => ne. by move: xi; rewrite ne setIf_0 => /in_set0. by apply: (setIf_i ne) => j jd; rewrite LgV //; move: (p1 _ jd) => []. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)