∀ {X : Type u_1} {Y : Type u_2} (motive : X ⊕ Y → X ⊕ Y → Sort u_3) (x : X) (y : Y)
  (h_1 : (x y : X) → motive (Sum.inl x) (Sum.inl y)) (h_2 : (x y : Y) → motive (Sum.inr x) (Sum.inr y))
  (h_3 : (x : X) → (y : Y) → motive (Sum.inl x) (Sum.inr y)) (h_4 : (x : Y) → (y : X) → motive (Sum.inr x) (Sum.inl y)),
  (match Sum.inl x, Sum.inr y with
    | Sum.inl x, Sum.inl y => h_1 x y
    | Sum.inr x, Sum.inr y => h_2 x y
    | Sum.inl x, Sum.inr y => h_3 x y
    | Sum.inr x, Sum.inl y => h_4 x y) =
    h_3 x y