proposition: Theorem dirim_setIf I f g: sub (direct_image g (intersectionf I f)) (intersectionf I (fun i => direct_image g (f i))).
proof: Proof. move => t /dirim_P [x]. case: (emptyset_dichot I) => neI; first by rewrite neI setIf_0 => /in_set0. move => ta tb; apply: (setIf_i neI) => j jI; apply/dirim_P; ex_tac. apply: setIf_hi ta jI. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)