proposition: Lemma setUf_P x I f: inc x (unionf I f) <-> exists2 y, inc y I & inc x (f y).
proof: Proof. split;first by move/setUt_P=> [z zp]; exists (Ro z) =>//; apply: R_inc. by move=>[y yi xf]; apply/setUt_P; exists (Bo yi); rewrite B_eq. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)