proposition: Lemma setUt_S (I:Set) (f g:I->Set): (forall i, sub (f i) (g i)) -> sub (uniont f) (uniont g).
proof: Proof. by move=> su t /setUt_P [z tf]; apply/setUt_P; exists z; apply: su. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)