proposition: Theorem setCUt2 (I:Set) (f:I-> Set) x: nonempty I -> x -s (uniont f) = intersectiont (fun i=> x -s (f i)).
proof: Proof. move=>neI; set_extens z. move /setC_P =>[zx zu];apply:(setIt_i neI) => j; apply setC_i => //. by dneg t; apply/ setUt_P; exists j. move: neI=> [_ [i _]] xi; move: (setIt_hi i xi) => /setC_P [zx zu]. apply: setC_i => //;move /setUt_P => [j zj]. by move: (setIt_hi j xi) => /setC_P [_]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)