∀ {J : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} J] (k k' : J) (motive : (∃ Z x x, True) → Prop)
  (x : ∃ Z x x, True), (∀ (l : J) (fl : k ⟶ l) (gl : k' ⟶ l) (h : True), motive ⋯) → motive x