proposition: Lemma setU2_A: associative union2.
proof: Proof. move => a b c; rewrite setU2_C. set_extens t; case /setU2_P; (try case /setU2_P); move => tx; apply/setU2_P;fprops; left; apply/setU2_P;fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)