{G : Group} (H K : Subgroup G) : Subgroup G. Proof. snrapply Build_Subgroup'. 1: exact (fun g => H g /\ K g). 1: exact _. 1: split; apply subgroup_in_unit. intros x y [] []. split; by apply subgroup_in_op_inv. Defined.
Require Import Basics Types HFiber WildCat.Core. Require Import Truncations.Core. Require Import Algebra.Groups.Group TruncType.