proposition: Lemma setCC_l A B C : (A -s B) -s C = A -s (B \cup C).
proof: Proof. set_extens t; case /setC_P. by case /setC_P => ta tb tc; apply/setC_P; split; [ | case/setU2_P ]. move => ta /setU2_ni [tb tc]; apply/setC_P;fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)