proposition: Lemma morphicP : reflect {in A &, {morph f : x y / x * y}} (morphic f).
proof: Proof. apply: (iffP forallP) => [fM x y Ax Ay | fM [x y] /=]. by apply/eqP; have:= fM (x, y); rewrite inE /= Ax Ay. by apply/implyP=> /andP[Ax Ay]; rewrite fM. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)