proposition: Lemma FreeGroup_rec_beta {G : Group} (f : A -> G) : FreeGroup_rec _ f o freegroup_in == f.
proof: Proof. intros x. apply grp_unit_r. Defined.
imports: Basics Types Group Subgroup WildCat.Core Colimits.Coeq Truncations.Core Truncations.SeparatedTrunc Classes.implementations.list