∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop}
  {motive : (a a_1 : α ⊕ β) → Sum.Lex r s a a_1 → Prop} {a a_1 : α ⊕ β} (t : Sum.Lex r s a a_1),
  (∀ {a₁ a₂ : α} (h : r a₁ a₂), motive (Sum.inl a₁) (Sum.inl a₂) ⋯) →
    (∀ {b₁ b₂ : β} (h : s b₁ b₂), motive (Sum.inr b₁) (Sum.inr b₂) ⋯) →
      (∀ (a : α) (b : β), motive (Sum.inl a) (Sum.inr b) ⋯) → motive a a_1 t