{G : Group} (H : Subgroup G) : Type := forall x, H x <-> trivial_subgroup x.
Require Import Basics Types HFiber WildCat.Core. Require Import Truncations.Core. Require Import Algebra.Groups.Group TruncType.