fact: Record GroupPresentation := { gp_generators : Type ; gp_rel_index : Type ; gp_relators : gp_rel_index -> FreeGroup gp_generators; }.
imports: Basics Types Truncations.Core Algebra.Groups.Group Algebra.Groups.FreeGroup Algebra.Groups.GroupCoeq Spaces.Finite WildCat