proposition: Lemma setUt_1 (a:Set) (x:a) (f: singleton (Ro x) -> Set): uniont f = f (Bo (set1_1 (Ro x))).
proof: Proof. set_extens t => pt; last by apply/setUt_P; exists (Bo (set1_1 (Ro x))). move /setUt_P: pt => [y tfy]. have <- //: (y = (Bo (set1_1 (Ro x)))). by apply: R_inj; move: (R_inc y) => /set1_P ->; rewrite B_eq. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)