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