fact: Definition subgroup_generated_gen_incl {G : Group} {X : G -> Type} (g : G) (H : X g) : subgroup_generated X := (g; tr (sgt_in H)).
imports: Basics Types HFiber WildCat.Core Truncations.Core Algebra.Groups.Group TruncType