proposition: Lemma setCI2_l A B C : (A \cap B) -s C = (A -s C) \cap (B -s C).
proof: Proof. set_extens t. by case/setC_P;case/setI2_P => ta tb tc; apply/setI2_P;split; apply/setC_P. case/setI2_P => /setC_P [ta tc] /setC_P [tb _]; apply/setC_P; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)