sgt_inv' {G : Group} {X} {g : G} : subgroup_generated_type X (- g) -> subgroup_generated_type X g. Proof. intros p. rewrite <- grp_inv_inv. by apply sgt_inv. Defined.
Require Import Basics Types HFiber WildCat.Core. Require Import Truncations.Core. Require Import Algebra.Groups.Group TruncType.