proposition: Lemma funI_setU f X: fun_image (union X) f = union (fun_image X (fun_image^~ f)).
proof: Proof. set_extens t. move /funI_P => [y /setU_P[x yx xz] ->]. by apply/setU_P; exists (fun_image x f); apply:funI_i. move/setU_P => [x tx /funI_P [y yz dy]]. move:tx; rewrite dy; move/funI_P => [u ua ->]; apply: funI_i. apply (setU_i ua yz). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)