proposition: Lemma setCI2_pr1 A B E: sub A E -> A -s B = A \cap (E -s B).
proof: Proof. move => ae; set_extens t. case /setC_P => ta tb; apply/setI2_P; split; first by exact. by apply/setC_P; split; [ apply: ae |]. case /setI2_P => ta /setC_P [_] tb; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)