proposition: Lemma setI2_A: associative intersection2.
proof: Proof. move => A B C; rewrite setI2_C. set_extens t; case /setI2_P; case /setI2_P=> tx ty tz; apply/setI2_P;fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)