∀ (x : CategoryTheory.Cat) (motive : ↑((CategoryTheory.Cat.objects.comp CategoryTheory.typeToCat).obj x) → Prop)
  (h : ↑((CategoryTheory.Cat.objects.comp CategoryTheory.typeToCat).obj x)),
  (∀ (as : CategoryTheory.Cat.objects.obj x), motive { as := as }) → motive h