{G : Type u_1} →
  [inst : CategoryTheory.Groupoid G] →
    {motive : IsFreeGroupoid G → Sort u} →
      ((quiverGenerators : Quiver (IsFreeGroupoid.Generators G)) →
          (of :
              {a b : IsFreeGroupoid.Generators G} →
                (a ⟶ b) →
                  ((have this := a;
                    this) ⟶
                    b)) →
            (unique_lift :
                ∀ {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 (of g) = f g) →
              motive { quiverGenerators := quiverGenerators, of := of, unique_lift := unique_lift }) →
        (t : IsFreeGroupoid G) → motive t