(G : Group) := { normalsubgroup_subgroup : Subgroup G ; normalsubgroup_isnormal : IsNormalSubgroup normalsubgroup_subgroup ; }.
Require Import Basics Types HFiber WildCat.Core. Require Import Truncations.Core. Require Import Algebra.Groups.Group TruncType.