proposition: Lemma distrib_prod2_sum A f: A \times (unionb f) = unionb (Lg (domain f) (fun x => A \times (Vg f x))).
proof: Proof. set_extens t. move=> /setX_P [pt ptA] /setUb_P [y ydf Qv]; apply/setUb_P; aw; ex_tac. by rewrite LgV //; apply :setX_i. move/setUb_P; aw; move=> [y ydf]; rewrite LgV //; move=> /setX_P [pr PA QV]. by apply/setX_P; split => //;apply /setUb_P;exists y. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)