proposition: Lemma eq_morphim (g : {morphism D >-> rT}): {in D, f =1 g} -> forall A, f @* A = g @* A.
proof: Proof. by move=> efg A; apply: eq_in_imset; apply: sub_in1 efg => x /setIP[]. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)