proposition: Lemma setUt_exten (I:Set) (f: I-> Set) (f':I->Set): f =1 f' -> uniont f = uniont f'.
proof: Proof. move=> hyp; set_extens t; move/setUt_P=> [z zi]; apply/setUt_P; exists z. by rewrite -hyp. by rewrite hyp. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)