proposition: Lemma setX0 (gT : 'I_0 -> finGroupType) (G : forall i, {group gT i}) : setXn G = 1%g.
proof: Proof. apply/setP => x; rewrite !inE; apply/forallP/idP => [_|? []//]. by apply/eqP/ffunP => -[]. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra all_solvable) mathcomp(all_field)