proposition: Corollary morph_eltr (gT : finGroupType) (f g : {morphism 'SG_n >-> gT}) : (forall i : 'I_n0, f 's_i = g 's_i) -> f =1 g.
proof: Proof. move=> Heq; elim/eltr_ind => [| s i lt_i_n0]; first by rewrite !morph1. by rewrite !morphM ?inE // (Heq (Ordinal lt_i_n0)) => ->. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) mathcomp(ssralg poly ssrint) permcomp tools permuted combclass congr