proposition: Lemma setUt_sub2 (I:Set) (f: I-> Set) x: nonempty I -> (forall i, sub x (f i)) -> sub x (uniont f).
proof: Proof. by move=> [y yI] hyp t tx; apply/setUt_P; exists (Bo yI);apply: hyp. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)