proposition: Lemma distrib_product2_inter f g: (intersectionb f) \times (intersectionb g) = intersectionf((domain f) \times (domain g)) (fun z => ((Vg f (P z)) \times (Vg g (Q z)))).
proof: Proof. move: (distrib_prod2_inter f g); rewrite / product2=> distr. set_extens x => xp. set (qx := variantLc (P x) (Q x)). have: inc qx (productb (variantLc (intersectionb f) (intersectionb g))). move /setX_P: xp =>[xp pxf qxg]; apply/setXf_P. rewrite /qx /C2; aw;split; fprops. by move=> i ind; try_lvariant ind. move: distr; rewrite /productf -variantLc_prop; move=> -> qxp. case: (emptyset_dichot (domain f \times domain g)) => xx. by move: qxp; rewrite xx setIf_0 => /in_set0. apply /(setIf_P _ xx)=> j jp;move /setXf_P : (setIf_hi qxp jp)=> [fgq dq vq]. move /setX_P : xp => [pa pb pc]; apply/setX_P. move: (vq _ inc_C0_C2)(vq _ inc_C1_C2); rewrite /qx;aw;split;fprops. set (qx := variantLc (P x) (Q x)). case: (emptyset_dichot (domain f \times domain g)) => xx. by move: xp; rewrite xx setIf_0 => /in_set0. have: inc qx (productb (variantLc (intersectionb f) (intersectionb g))). move: distr; rewrite /productf variantLc_prop; move =>->. apply (setIf_i xx)=> j jp; move /setX_P: (setIf_hi xp jp) => [_ Px Qx]. apply/setXf_P; rewrite /qx;split; aww. move=> i it; try_lvariant it; fprops. move/setXf_P => [_ _]; rewrite /qx; aw => qv. move: xx=> [w wp]; move /setX_P: (setIf_hi xp wp) => [px _ _]; apply /setX_P. by move: (qv _ inc_C0_C2) (qv _ inc_C1_C2); aw. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)