∀ {B : Type u} [inst : Quiver B]
  {motive :
    {a b : CategoryTheory.FreeBicategory B} →
      {f g : a ⟶ b} →
        (a_1 a_2 : CategoryTheory.FreeBicategory.Hom₂ f g) → CategoryTheory.FreeBicategory.Rel a_1 a_2 → Prop}
  {motive_1 :
    {a b : CategoryTheory.FreeBicategory B} →
      {f g : a ⟶ b} →
        {a_1 a_2 : CategoryTheory.FreeBicategory.Hom₂ f g} →
          (t : CategoryTheory.FreeBicategory.Rel a_1 a_2) → CategoryTheory.FreeBicategory.Rel.below t → Prop}
  {a b : CategoryTheory.FreeBicategory B} {f g : a ⟶ b} {a_1 a_2 : CategoryTheory.FreeBicategory.Hom₂ f g}
  {t : CategoryTheory.FreeBicategory.Rel a_1 a_2} (t_1 : CategoryTheory.FreeBicategory.Rel.below t),
  (∀ {a b : B} {f g h : CategoryTheory.FreeBicategory.Hom a b} (η : CategoryTheory.FreeBicategory.Hom₂ f g)
      (θ₁ θ₂ : CategoryTheory.FreeBicategory.Hom₂ g h) (a_3 : CategoryTheory.FreeBicategory.Rel θ₁ θ₂)
      (ih : CategoryTheory.FreeBicategory.Rel.below a_3) (a_ih : motive θ₁ θ₂ a_3), motive_1 ⋯ ⋯) →
    (∀ {a b : B} {f g h : CategoryTheory.FreeBicategory.Hom a b} (η₁ η₂ : CategoryTheory.FreeBicategory.Hom₂ f g)
        (θ : CategoryTheory.FreeBicategory.Hom₂ g h) (a_3 : CategoryTheory.FreeBicategory.Rel η₁ η₂)
        (ih : CategoryTheory.FreeBicategory.Rel.below a_3) (a_ih : motive η₁ η₂ a_3), motive_1 ⋯ ⋯) →
      (∀ {a b : B} {f g : CategoryTheory.FreeBicategory.Hom a b} (η : CategoryTheory.FreeBicategory.Hom₂ f g),
          motive_1 ⋯ ⋯) →
        (∀ {a b : B} {f g : CategoryTheory.FreeBicategory.Hom a b} (η : CategoryTheory.FreeBicategory.Hom₂ f g),
            motive_1 ⋯ ⋯) →
          (∀ {a b : B} {f g h i : CategoryTheory.FreeBicategory.Hom a b} (η : CategoryTheory.FreeBicategory.Hom₂ f g)
              (θ : CategoryTheory.FreeBicategory.Hom₂ g h) (ι : CategoryTheory.FreeBicategory.Hom₂ h i), motive_1 ⋯ ⋯) →
            (∀ {a b c : B} (f : CategoryTheory.FreeBicategory.Hom a b) (g h : CategoryTheory.FreeBicategory.Hom b c)
                (η η' : CategoryTheory.FreeBicategory.Hom₂ g h) (a_3 : CategoryTheory.FreeBicategory.Rel η η')
                (ih : CategoryTheory.FreeBicategory.Rel.below a_3) (a_ih : motive η η' a_3), motive_1 ⋯ ⋯) →
              (∀ {a b c : B} (f : CategoryTheory.FreeBicategory.Hom a b) (g : CategoryTheory.FreeBicategory.Hom b c),
                  motive_1 ⋯ ⋯) →
                (∀ {a b c : B} (f : CategoryTheory.FreeBicategory.Hom a b)
                    {g h i : CategoryTheory.FreeBicategory.Hom b c} (η : CategoryTheory.FreeBicategory.Hom₂ g h)
                    (θ : CategoryTheory.FreeBicategory.Hom₂ h i), motive_1 ⋯ ⋯) →
                  (∀ {a b : B} {f g : CategoryTheory.FreeBicategory.Hom a b}
                      (η : CategoryTheory.FreeBicategory.Hom₂ f g), motive_1 ⋯ ⋯) →
                    (∀ {a b c d : B} (f : CategoryTheory.FreeBicategory.Hom a b)
                        (g : CategoryTheory.FreeBicategory.Hom b c) {h h' : CategoryTheory.FreeBicategory.Hom c d}
                        (η : CategoryTheory.FreeBicategory.Hom₂ h h'), motive_1 ⋯ ⋯) →
                      (∀ {a b c : B} (f g : CategoryTheory.FreeBicategory.Hom a b)
                          (h : CategoryTheory.FreeBicategory.Hom b c) (η η' : CategoryTheory.FreeBicategory.Hom₂ f g)
                          (a_3 : CategoryTheory.FreeBicategory.Rel η η')
                          (ih : CategoryTheory.FreeBicategory.Rel.below a_3) (a_ih : motive η η' a_3), motive_1 ⋯ ⋯) →
                        (∀ {a b c : B} (f : CategoryTheory.FreeBicategory.Hom a b)
                            (g : CategoryTheory.FreeBicategory.Hom b c), motive_1 ⋯ ⋯) →
                          (∀ {a b c : B} {f g h : CategoryTheory.FreeBicategory.Hom a b}
                              (i : CategoryTheory.FreeBicategory.Hom b c) (η : CategoryTheory.FreeBicategory.Hom₂ f g)
                              (θ : CategoryTheory.FreeBicategory.Hom₂ g h), motive_1 ⋯ ⋯) →
                            (∀ {a b : B} {f g : CategoryTheory.FreeBicategory.Hom a b}
                                (η : CategoryTheory.FreeBicategory.Hom₂ f g), motive_1 ⋯ ⋯) →
                              (∀ {a b c d : B} {f f' : CategoryTheory.FreeBicategory.Hom a b}
                                  (g : CategoryTheory.FreeBicategory.Hom b c)
                                  (h : CategoryTheory.FreeBicategory.Hom c d)
                                  (η : CategoryTheory.FreeBicategory.Hom₂ f f'), motive_1 ⋯ ⋯) →
                                (∀ {a b c d : B} (f : CategoryTheory.FreeBicategory.Hom a b)
                                    {g g' : CategoryTheory.FreeBicategory.Hom b c}
                                    (η : CategoryTheory.FreeBicategory.Hom₂ g g')
                                    (h : CategoryTheory.FreeBicategory.Hom c d), motive_1 ⋯ ⋯) →
                                  (∀ {a b c : B} {f g : CategoryTheory.FreeBicategory.Hom a b}
                                      {h i : CategoryTheory.FreeBicategory.Hom b c}
                                      (η : CategoryTheory.FreeBicategory.Hom₂ f g)
                                      (θ : CategoryTheory.FreeBicategory.Hom₂ h i), motive_1 ⋯ ⋯) →
                                    (∀ {a b c d : B} (f : CategoryTheory.FreeBicategory.Hom a b)
                                        (g : CategoryTheory.FreeBicategory.Hom b c)
                                        (h : CategoryTheory.FreeBicategory.Hom c d), motive_1 ⋯ ⋯) →
                                      (∀ {a b c d : B} (f : CategoryTheory.FreeBicategory.Hom a b)
                                          (g : CategoryTheory.FreeBicategory.Hom b c)
                                          (h : CategoryTheory.FreeBicategory.Hom c d), motive_1 ⋯ ⋯) →
                                        (∀ {a b : B} (f : CategoryTheory.FreeBicategory.Hom a b), motive_1 ⋯ ⋯) →
                                          (∀ {a b : B} (f : CategoryTheory.FreeBicategory.Hom a b), motive_1 ⋯ ⋯) →
                                            (∀ {a b : B} (f : CategoryTheory.FreeBicategory.Hom a b), motive_1 ⋯ ⋯) →
                                              (∀ {a b : B} (f : CategoryTheory.FreeBicategory.Hom a b), motive_1 ⋯ ⋯) →
                                                (∀ {a b c d e : B} (f : CategoryTheory.FreeBicategory.Hom a b)
                                                    (g : CategoryTheory.FreeBicategory.Hom b c)
                                                    (h : CategoryTheory.FreeBicategory.Hom c d)
                                                    (i : CategoryTheory.FreeBicategory.Hom d e), motive_1 ⋯ ⋯) →
                                                  (∀ {a b c : B} (f : CategoryTheory.FreeBicategory.Hom a b)
                                                      (g : CategoryTheory.FreeBicategory.Hom b c), motive_1 ⋯ ⋯) →
                                                    motive_1 t t_1