proposition: Lemma partition_product f: (forall l, inc l (domain f) -> (partition_w_fam (Vg f l) (unionb (Vg f l)))) -> partition_w_fam(Lg(productf (domain f) (fun l => domain (Vg f l)) ) (fun g => (productf (domain f) (fun l => Vg (Vg f l) (Vg g l))))) ( productf (domain f) (fun l => unionb (Vg f l))).
proof: Proof. move=> alp;split; first by fprops. move=> i j; rewrite Lgd => ip jp; rewrite ! LgV //. alt_tac ij. hnf; set int:= _ \cap _. case: (emptyset_dichot int) =>// ei. case: ij; move: ei=> [xi]; rewrite/int; aw. move: ip jp => /setXf_P [fi di vi] /setXf_P [fj dj vj] /setI2_P [] /setXf_P [fx dx eq1] /setXf_P [_ _ eq2]. apply: fgraph_exten =>//; try ue. move=> x; rewrite di => xd; move: (eq1 _ xd) (eq2 _ xd) (alp _ xd). rewrite /partition_w_fam; move=> eq3 eq4 [fgV md _]. move: (vi _ xd) (vj _ xd)=> eq5 eq6; case: (md _ _ eq5 eq6) =>// dij. empty_tac1 (Vg xi x). rewrite distrib_prod_union /unionb;aw;apply: setUf_exten =>// i ip. by rewrite LgV. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)