∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] {W : CategoryTheory.MorphismProperty C}
  {motive :
    ⦃X Y : CategoryTheory.Paths (CategoryTheory.Localization.Construction.LocQuiver W)⦄ →
      (a a_1 : X ⟶ Y) → CategoryTheory.Localization.Construction.relations W a a_1 → Prop}
  ⦃X Y : CategoryTheory.Paths (CategoryTheory.Localization.Construction.LocQuiver W)⦄ {a a_1 : X ⟶ Y}
  (t : CategoryTheory.Localization.Construction.relations W a a_1),
  (∀ (X : C),
      motive (CategoryTheory.Localization.Construction.ψ₁ W (CategoryTheory.CategoryStruct.id X))
        (CategoryTheory.CategoryStruct.id (CategoryTheory.Localization.Construction.ιPaths W X)) ⋯) →
    (∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z),
        motive (CategoryTheory.Localization.Construction.ψ₁ W (CategoryTheory.CategoryStruct.comp f g))
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Localization.Construction.ψ₁ W f)
            (CategoryTheory.Localization.Construction.ψ₁ W g))
          ⋯) →
      (∀ {X Y : C} (w : X ⟶ Y) (hw : W w),
          motive
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.Localization.Construction.ψ₁ W w)
              (CategoryTheory.Localization.Construction.ψ₂ W w hw))
            (CategoryTheory.CategoryStruct.id (CategoryTheory.Localization.Construction.ιPaths W X)) ⋯) →
        (∀ {X Y : C} (w : X ⟶ Y) (hw : W w),
            motive
              (CategoryTheory.CategoryStruct.comp (CategoryTheory.Localization.Construction.ψ₂ W w hw)
                (CategoryTheory.Localization.Construction.ψ₁ W w))
              (CategoryTheory.CategoryStruct.id (CategoryTheory.Localization.Construction.ιPaths W Y)) ⋯) →
          motive a a_1 t