proposition: Lemma inj_image_setIf I f g: injection g -> (Vfs g (intersectionf I f)) = (intersectionf I (fun i => Vfs g (f i))).
proof: Proof. move=> ig; move: (proj1 ig) => fg. have [_ _ _ _ aux]:= (canonical_decomposition1 fg). have sf := (iim_fun_r fg). rewrite sf iim_fun_setIf; last by apply: (bijective_inv_f (aux ig)). by apply: setIf_exten. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)