∀ (C : Type u_2) (D : Type u_1) [inst : CategoryTheory.Category.{u_3, u_2} C]
  [inst_1 : CategoryTheory.Category.{u_4, u_1} D] (motive : (CategoryTheory.Join C D)ᵒᵖ → Prop)
  (x : (CategoryTheory.Join C D)ᵒᵖ),
  (∀ (a : C), motive (Opposite.op (CategoryTheory.Join.left a))) →
    (∀ (a : D), motive (Opposite.op (CategoryTheory.Join.right a))) → motive x