proposition: Lemma distrib_inter2_union f g: (unionb f) \cap (unionb g) = unionf((domain f) \times (domain g)) (fun z => ((Vg f (P z)) \cap (Vg g (Q z)))).
proof: Proof. set_extens x. move /setI2_P => [] /setUb_P [y yd xf] /setUb_P [z zd xg]. apply/setUf_P; exists (J y z);aw; fprops. move /setUf_P=> [y /setX_P [yp yf yg] /setI2_P [pa pb]]. apply/setI2_P; split; union_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)