{G : Group} (H1 H2 : Subgroup G) : H1 = H2 -> GroupIsomorphism H1 H2 := ltac:(intros []; exact grp_iso_id).
Require Import Basics Types HFiber WildCat.Core. Require Import Truncations.Core. Require Import Algebra.Groups.Group TruncType.