proposition: Lemma setPI : morphism_2 powerset intersection2 intersection2.
proof: Proof. move => A B; set_extens t. move/setP_P /subsetI2_P => [ta tb];apply/setI2_P. by split; apply/setP_P. by move /setI2_P=> [ta tb]; apply/setP_P; apply: setI2_12S;apply/setP_P. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)