proposition: Theorem setUt_rewrite (I K:Set) (f: K->I) (g:I ->Set): (forall u, exists v, f v = u) -> uniont g = uniont (g \o f).
proof: Proof. move=> sf; set_extens t; move/setUt_P=> [z zp]; apply/setUt_P. by move: (sf z) => [v fv] /=; exists v; ue. by exists (f z). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)