∀ {α₁ : Type u_1} {α₂ : Type u_2} {β₁ : Type u_3} {β₂ : Type u_4} (motive : α₁ ⊕ α₂ → β₁ ⊕ β₂ → Sort u_5) (val : α₁)
  (val_1 : β₂) (h_1 : (a : α₁) → (b : β₁) → motive (Sum.inl a) (Sum.inl b))
  (h_2 : (val : α₁) → (val_2 : β₂) → motive (Sum.inl val) (Sum.inr val_2))
  (h_3 : (val : α₂) → (val_2 : β₁) → motive (Sum.inr val) (Sum.inl val_2))
  (h_4 : (a : α₂) → (b : β₂) → motive (Sum.inr a) (Sum.inr b)),
  (match Sum.inl val, Sum.inr val_1 with
    | Sum.inl a, Sum.inl b => h_1 a b
    | Sum.inl val, Sum.inr val_2 => h_2 val val_2
    | Sum.inr val, Sum.inl val_2 => h_3 val val_2
    | Sum.inr a, Sum.inr b => h_4 a b) =
    h_2 val val_1