proposition: Lemma distrib_prod2_union f g: product2 (unionb f)(unionb g) = unionf((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 iV]. have Tat: inc C0 C2 by fprops. have Tbt: inc C1 C2 by fprops. move: (iV _ Tat) (iV _ Tbt); aw. move=> /setUb_P [u ud uVV] /setUb_P [v vd vVV]; apply/setUf_P. exists (J u v); fprops; apply/setXf_P;split => //. by move=> i ind; try_lvariant ind; aw. move/setUf_P=>[y] /setX_P [yp py qy] /setXf_P [fx dx iV]; apply/setXf_P. split => // i idx; move: (iV _ idx); try_lvariant idx; move=> ?; union_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)