∀ {G : Type u_1} {inst : CategoryTheory.Groupoid G} [self : IsFreeGroupoid G] {X : Type v} [inst_1 : Group X]
  (f : Quiver.Labelling (IsFreeGroupoid.Generators G) X),
  ∃! F, ∀ (a b : IsFreeGroupoid.Generators G) (g : a ⟶ b), F.map (IsFreeGroupoid.of g) = f g