proposition: Theorem setCIt2 (I:Set) (f:I-> Set) x: nonempty I -> x -s (intersectiont f) = uniont (fun i=> x -s (f i)).
proof: Proof. move=> neI. set_extens t. move/setC_P => [tx ti]; apply/setUt_P; ex_middle bad. case: ti; apply /(setIt_P _ neI) => j;ex_middle bad2. case: bad; exists j; apply: setC_i => //. move/setUt_P => [z /setC_P [tx tf]];apply: setC_i => // h. exact:(tf (setIt_hi z h)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)