proposition: Lemma setUt_P (I:Set) (f:I->Set) x: inc x (uniont f) <-> exists z, inc x (f z).
proof: Proof. split; first by move/IM_P=>[a ->]; case: a => b fb; exists b; apply: R_inc. by move => [z xf]; apply /IM_P;exists (Uaux_c (Bo xf)); rewrite B_eq. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)