∀ (C : Type u_2) [inst : CategoryTheory.Category.{u_1, u_2} C] {x y : C}
  (motive : CategoryTheory.IsIsomorphic x y → Prop) (x_1 : CategoryTheory.IsIsomorphic x y),
  (∀ (α : x ≅ y), motive ⋯) → motive x_1