∀ {J : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} J]
  (motive : (x x_1 : CategoryTheory.WithTerminal J) → (x ⟶ x_1) → Prop) (x x_1 : CategoryTheory.WithTerminal J)
  (x_2 : x ⟶ x_1),
  (∀ (x : CategoryTheory.WithTerminal.star ⟶ CategoryTheory.WithTerminal.star),
      motive CategoryTheory.WithTerminal.star CategoryTheory.WithTerminal.star x) →
    (∀ (a : J) (x : CategoryTheory.WithTerminal.of a ⟶ CategoryTheory.WithTerminal.star),
        motive (CategoryTheory.WithTerminal.of a) CategoryTheory.WithTerminal.star x) →
      (∀ (a b : J) (f : CategoryTheory.WithTerminal.of a ⟶ CategoryTheory.WithTerminal.of b),
          motive (CategoryTheory.WithTerminal.of a) (CategoryTheory.WithTerminal.of b) f) →
        motive x x_1 x_2