fact: Definition sgt_op' {G : Group} {X} {g h : G} : subgroup_generated_type X g -> subgroup_generated_type X h -> subgroup_generated_type X (g * h).
imports: Basics Types HFiber WildCat.Core Truncations.Core Algebra.Groups.Group TruncType