proposition: Theorem setIt_rewrite (I K:Set) (f: K->I) (g:I ->Set): (forall u, exists v, f v = u) -> intersectiont g = intersectiont (g \o f).
proof: Proof. move=> sf; case: (emptyset_dichot I) => ei. rewrite ! setIt_0 =>//; apply /set0_P => y [x _]. move: (f x); rewrite ei; case. have nek: nonempty K. move: ei => [k [i]] _; move: (sf i)=> [j _]; exists (Ro j); apply: R_inc. set_extens t; move/setIt_P=> h; apply/setIt_P => // j; first by apply: (h ei). move: (sf j) => [k <-]; exact: (h nek k). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)