∀ (C : Type u_4) (D : Type u_2) [inst : CategoryTheory.Category.{u_3, u_4} C]
  [inst_1 : CategoryTheory.Category.{u_1, u_2} D] {c c' : Cᵒᵖ} {d d' : Dᵒᵖ} (motive : (d ⟶ d') → (c ⟶ c') → Prop)
  (x : d ⟶ d') (x_1 : c ⟶ c'),
  (∀ (f : Opposite.unop d' ⟶ Opposite.unop d) (g : Opposite.unop c' ⟶ Opposite.unop c),
      motive (Opposite.op f) (Opposite.op g)) →
    motive x x_1