proposition: Lemma setIt_1 (a:Set)(x:a) (f: singleton (Ro x) -> Set): intersectiont f = f (Bo (set1_1 (Ro x))).
proof: Proof. apply: extensionality; first by apply:setIt_s1. move => t ti; apply: setIt_i;[by fprops | move=> j]. have -> //: (j = (Bo (set1_1 (Ro x)))). by apply: R_inj; move: (R_inc j) => /set1_P ->; rewrite B_eq. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)