proposition: Lemma setCUf2 I f x: nonempty I -> x -s (unionf I f) = intersectionf I (fun i=> x -s (f i)).
proof: Proof. move => neI; set_extens z. move /setC_P =>[zx zu];apply:(setIf_i neI) => j jI; apply setC_i => //. dneg t; union_tac. move: neI=> [i iI] xi; move: (setIf_hi xi iI) => /setC_P [zx zu]. apply: setC_i => // /setUf_P [j jI zj]. by case/setC_P: (setIf_hi xi jI). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)