proposition: Lemma homgP rT aT (C : {set rT}) (D : {set aT}) : reflect (exists f : {morphism D >-> rT}, f @* D = C) (homg C D).
proof: Proof. apply: (iffP exists_eq_inP) => [[f fM <-] | [f <-]]. by exists (morphm_morphism fM); rewrite /morphim /= setIid. exists (finfun f); first by apply/morphicP=> x y Dx Dy; rewrite !ffunE morphM. by rewrite /morphim setIid; apply: eq_imset => x; rewrite ffunE. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)