∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_3, u_1} C] {P Q : CategoryTheory.ObjectProperty C}
  (motive : Subtype P ⊕ Subtype Q → Sort u_2) (x : Subtype Q) (h_1 : (x : Subtype P) → motive (Sum.inl x))
  (h_2 : (x : Subtype Q) → motive (Sum.inr x)),
  (match Sum.inr x with
    | Sum.inl x => h_1 x
    | Sum.inr x => h_2 x) =
    h_2 x