{S : Type} {F_S : Group} {i : S -> F_S} `{IsFreeGroupOn S F_S i} {G : Group} (f : S -> G) : isfreegroupon_rec f o i == f := (center (FactorsThroughFreeGroup S F_S i G f)).
Require Import Basics Types Group Subgroup