proposition: Lemma morphim_gen A : A \subset D -> f @* <<A>> = <<f @* A>>.
proof: Proof. move=> sAD; apply/eqP. rewrite eqEsubset andbC gen_subG morphimS; last exact: subset_gen. by rewrite sub_morphim_pre gen_subG // -sub_morphim_pre // subset_gen. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)