proposition: Lemma setCIf2 I f x: nonempty I -> x -s (intersectionf I f) = unionf I (fun i=> x -s (f i)).
proof: Proof. move=> neI;set_extens t. move/setC_P => [tx ti]; apply/setUf_P; ex_middle bad. case: ti;apply /(setIf_P f neI) => j jI;ex_middle bad2. by case: bad; exists j => //; apply: setC_i. move/setUf_P => [z zI /setC_P [tx tf]];apply: setC_i => // h. exact:(tf (setIf_hi h zI)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)