(P : FreeGroup -> Type) `{forall x, IsHProp (P x)} (H1 : P mon_unit) (Hin : forall x, P (freegroup_in x)) (Hop : forall x y, P x -> P y -> P (- x * y)) : forall x, P x. Proof. rapply '. intros w. induction w as [|a w IHw]. - exact H1. - destruct a as [a|a]. + change (P ((freegroup_in a) * freegroup_eta w)). rewrite <- (grp_inv_inv a). apply Hop. * rewrite <- grp_unit_r. by apply Hop. * assumption. + change (P (-(freegroup_in a) * freegroup_eta w)). by apply Hop. Defined.
Require Import Basics Types Group Subgroup