∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {G : Type u₁} [inst_1 : CategoryTheory.Groupoid G]
  (φ : CategoryTheory.Functor C G), (CategoryTheory.FreeGroupoid.of C).comp (CategoryTheory.FreeGroupoid.lift φ) = φ