sgt_op' {G : Group} {X} {g h : G} : subgroup_generated_type X g -> subgroup_generated_type X h -> subgroup_generated_type X (g * h). Proof. intros p q. rewrite <- (negate_involutive h). exact (sgt_op p (sgt_inv q)). Defined.
Require Import Basics Types HFiber WildCat.Core. Require Import Truncations.Core. Require Import Algebra.Groups.Group TruncType.