proposition: Lemma set2_IXl: left_distributive product intersection2.
proof: Proof. move => a b c;set_extens x. by move/setX_P => [Px /setI2_P [pa pb] xa]; apply/setI2_P;split;apply/setX_P. move /setI2_P => [] /setX_P [Px px qx1 /setX_P [_ qx2 _]]. apply/setX_P; split; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)