{G : Group} (H K : Subgroup G) : Subgroup G := subgroup_generated (fun x => ((H x) + (K x))%type).
Require Import Basics Types HFiber WildCat.Core. Require Import Truncations.Core. Require Import Algebra.Groups.Group TruncType.