FreeGroup_ind_hprop' (P : FreeGroup -> Type) `{forall x, IsHProp (P x)} (H1 : forall w, P (freegroup_eta w)) : forall x, P x. Proof. rapply Trunc_ind. srapply Coeq_ind_hprop. exact H1. Defined.
Require Import Basics Types Group Subgroup