∀ {G : Type u_1} [inst : CategoryTheory.Groupoid G] [inst_1 : IsFreeGroupoid G]
  (T : WideSubquiver (Quiver.Symmetrify (IsFreeGroupoid.Generators G)))
  [inst_2 : Quiver.Arborescence (WideSubquiver.toType (Quiver.Symmetrify (IsFreeGroupoid.Generators G)) T)]
  (motive :
    (x : G) →
      Quiver.Path (Quiver.root (WideSubquiver.toType (Quiver.Symmetrify (IsFreeGroupoid.Generators G)) T)) x → Sort u_2)
  (h_1 :
    Unit →
      motive (Quiver.root (WideSubquiver.toType (Quiver.Symmetrify (IsFreeGroupoid.Generators G)) T)) Quiver.Path.nil)
  (h_2 :
    (x b : WideSubquiver.toType (Quiver.Symmetrify (IsFreeGroupoid.Generators G)) T) →
      (p : Quiver.Path (Quiver.root (WideSubquiver.toType (Quiver.Symmetrify (IsFreeGroupoid.Generators G)) T)) b) →
        (f : b ⟶ x) → motive x (p.cons f)),
  (match Quiver.root (WideSubquiver.toType (Quiver.Symmetrify (IsFreeGroupoid.Generators G)) T), Quiver.Path.nil with
    | .(Quiver.root (WideSubquiver.toType (Quiver.Symmetrify (IsFreeGroupoid.Generators G)) T)), Quiver.Path.nil =>
      h_1 ()
    | x, p.cons f => h_2 x b p f) =
    h_1 ()