proposition: Theorem dirim_setUf I f g: direct_image g (unionf I f) = unionf I (fun i => direct_image g (f i)).
proof: Proof. set_extens t. move /dirim_P=> [x /setUf_P [y yI xfy] Ju]; apply /setUf_P. exists y => //; apply/dirim_P; ex_tac. move /setUf_P => [z zI /dirim_P [x xf Jg]]. apply /dirim_P;ex_tac; union_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)