proposition: Lemma distrib_inter_prod_inter f g: domain f = domain g -> product2 (intersectionb f) (intersectionb g) = intersectionf (domain f) (fun i => product2 (Vg f i) (Vg g i)).
proof: Proof. move=> dfdg; set (sb:= domain f). pose (h:= Lg (product C2 sb) (fun i => Yo (P i = C0) (Vg f(Q i)) (Vg g (Q i)))). move: C0_ne_C1 => ns. have <-: intersectionf sb(fun k => productf C2 (fun i => Vg h (J i k))) = intersectionf sb (fun i => product2 (Vg f i) (Vg g i)). apply: setIf_exten. move=> i isb /=; congr (productb _ );apply: Lg_exten=> x xp. rewrite /h; try_lvariant xp; rewrite LgV //; aw; try Ytac0 =>//; apply:setXp_i; fprops. have aux: nonempty C2 \/ nonempty sb by left; exists C0; fprops. rewrite (distrib_inter_prod h aux); congr (productb _);apply: Lg_exten=> x xp. try_lvariant xp; [ | rewrite /intersectionb - dfdg]; apply: setIf_exten; move => i id; rewrite LgV // ; aw; (try Ytac0 => //); apply:setXp_i; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)