proposition: Lemma distrib_prod2_inter f g: product2 (intersectionb f)(intersectionb g)= intersectionf((domain f)\times (domain g)) (fun z => (product2 (Vg f (P z)) (Vg g (Q z)))).
proof: Proof. rewrite/product2; set_extens x. move /setXf_P=> [fx dx iVv]. case: (emptyset_dichot (domain f \times domain g)) => xx. move: (iVv _ inc_C0_C2) (iVv _ inc_C1_C2); aw; rewrite /intersectionb. case: (setX_0 xx) => ->; rewrite setIf_0. by move => /in_set0. by move => _ /in_set0. apply :(setIf_i xx) => j. move/setX_P => [jp pj qj]; apply/setXf_P;split => // i id. move: (iVv _ id); try_lvariant id => Vi; first by apply: (setIf_hi Vi pj). by apply: (setIf_hi Vi qj). case: (emptyset_dichot (domain f \times domain g)) => xx. by rewrite xx setIf_0 => /in_set0. move/(setIf_P _ xx) => h. move: xx => [j jp]; move: (h _ jp) => /setXf_P [pa pb pc]. move /setX_P: jp => [_ ja jb]. have nef: nonempty f by apply /domain_set0P; ex_tac. have neg: nonempty g by apply /domain_set0P; ex_tac. have aux: (forall i j, inc i (domain f) -> inc j (domain g) -> (inc (Vg x C0) (Vg f i) /\ inc (Vg x C1) (Vg g j))). move=> i k id kd. have Jd: (inc (J i k) ((domain f) \times (domain g))) by fprops. move: (h _ Jd) => /setXf_P [fx dx px]. by move: (px _ inc_C0_C2)(px _ inc_C1_C2); aw; aw => qa qb; split. apply/setXf_P;split => // i itp; try_lvariant itp; apply setIb_i => // k kd. by move: (aux _ _ kd jb) => []. by move: (aux _ _ ja kd) => []. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)