proposition: Lemma distrib_product2_union f g: (unionb f) \times (unionb g) = unionf((domain f) \times (domain g)) (fun z => ((Vg f (P z)) \times (Vg g (Q z)))).
proof: Proof. move: (distrib_prod2_union f g); rewrite/product2 => distr. set_extens x. move /setX_P=> [xp px qx]. set (v := variantLc (P x) (Q x)). have: inc v (productb (variantLc (unionb f) (unionb g))). by apply/setXb_P;rewrite/v; aw; split; fprops => i it; try_lvariant it. rewrite /productf in distr; rewrite variantLc_prop distr. move /setUf_P => [y p1 p2]; apply/setUf_P; ex_tac. move /setXf_P: p2=> [fv]; aw => dv p; apply/setX_P. move: (p _ inc_C0_C2) (p _ inc_C1_C2); rewrite /v; aw; split;fprops. move /setUf_P=> [y yp /setX_P [px xp xq]]. set (qx := variantLc (P x) (Q x)). have:(inc qx (productb (variantLc (unionb f) (unionb g)))). move: distr; rewrite/productf -variantLc_prop; move=>->. union_tac; apply/setXf_P;rewrite /qx; aw;split; fprops. move=> i it; try_lvariant it; fprops. move/setXf_P=> [fq dx vqx]; apply/setX_P. by move: (vqx _ inc_C0_C2) (vqx _ inc_C1_C2); rewrite /qx;aw. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)