proposition: Lemma set2_UXl: left_distributive product union2.
proof: Proof. move => a b c; set_extens x. move /setX_P => [pa /setU2_P pb pc]. by case:pb => pb; apply /setU2_P; [left | right]; apply:setX_i. case /setU2_P => /setX_P [pa pb pc]; apply/setX_i => //; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)