proposition: Theorem distrib_prod_union f: productf (domain f) (fun l => unionb (Vg f l)) = unionf (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. case: (emptyset_dichot (domain f)) => p. by rewrite p /productf /Lg !funI_set0 !setXb_0 setUf_1 funI_set0 setXb_0. case: (p_or_not_p (forall l, inc l (domain f) -> nonempty (domain (Vg f l)))). move=> alned. set_extens x => xp; last first. move: xp => /setUf_P [y /setXf_P [fy dy py] /setXf_P [fx dx px]]. by apply/setXf_P;split => // i idf; apply: (@setUb_i _ (Vg y i)); fprops. move: xp=> /setXf_P [gx dx px]. have : (nonempty (productf (domain f) (fun l => (Zo (domain (Vg f l)) (fun i => (inc (Vg x l) (Vg (Vg f l) i))))))). apply: setXb_ne; fprops; hnf;hnf; aw;move=> i id; rewrite LgV//. by move /setUb_P: (px _ id) => [y yd iVV]; exists y; apply: Zo_i. move=> [y /setXf_P [fy dy py] ]. by apply: (@setUf_i _ y); apply/setXf_P; split => // i idf;case /Zo_P: (py _ idf). move=> special. have [x xd de]: exists2 l, inc l (domain f) & domain (Vg f l) = emptyset. ex_middle aux; case: special=> l ld. case: (emptyset_dichot (domain (Vg f l)))=>// pp. case: aux; ex_tac. have ->: productf (domain f) (fun l => domain (Vg f l)) = emptyset. apply /set0_P => t/setXf_P [pa pb pc]. by move: (pc _ xd); rewrite de => /in_set0. rewrite setUf_0;apply /set0_P => t /setXf_P [pa pb pc]. by move: (pc _ xd); move/domain_set0_P: de => ->;rewrite setUb_0 => /in_set0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)