proposition: Lemma fullv_lfunP (U : seq uT) (phi psi : 'Hom(uT,vT)) : <<U>>%VS = fullv -> phi = psi <-> {in U, phi =1 psi}.
proof: Proof. by move=> Uf; split=> [->//|/span_lfunP]; rewrite Uf=> /(_ _ (memvf _))-/lfunP. Qed.
imports: mathcomp(all_ssreflect all_fingroup all_algebra all_solvable)