proposition: Proposition equiv_path_subgroup `{F : Funext} {G : Group} (H K : Subgroup G) : (H == K) <~> (H = K).
proof: Proof. refine ((equiv_ap' issig_subgroup^-1%equiv _ _)^-1%equiv oE _); cbn. refine (equiv_path_sigma_hprop _ _ oE _); cbn. apply equiv_path_arrow. Defined.
imports: Basics Types HFiber WildCat.Core Truncations.Core Algebra.Groups.Group TruncType