{G : Group} {f f' : FreeGroup $-> G} (H : forall x, f (freegroup_in x) = f' (freegroup_in x)) : f $== f'. Proof. rapply FreeGroup_ind_hprop. - exact (concat (grp_homo_unit f) (grp_homo_unit f')^). - exact H. - intros x y p q. refine (grp_homo_op_agree f f' _ q). lhs nrapply grp_homo_inv. rhs nrapply grp_homo_inv. exact (ap _ p). Defined.
Require Import Basics Types Group Subgroup