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