proposition: Lemma dirim_setI2 g x y: sub (direct_image g (x \cap y)) ((direct_image g x) \cap (direct_image g y)).
proof: Proof. rewrite - setIf2f - setIf2; apply: dirim_setIf. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)