∀ {α : Type u_1} {γ : Type u_2} {β : Type u_3} {δ : Type u_4} {r : α → γ → Prop} {s : β → δ → Prop}
  {motive : (a : α ⊕ β) → (a_1 : γ ⊕ δ) → Sum.LiftRel r s a a_1 → Prop} {a : α ⊕ β} {a_1 : γ ⊕ δ}
  (t : Sum.LiftRel r s a a_1),
  (∀ {a : α} {c : γ} (a_2 : r a c), motive (Sum.inl a) (Sum.inl c) ⋯) →
    (∀ {b : β} {d : δ} (a : s b d), motive (Sum.inr b) (Sum.inr d) ⋯) → motive a a_1 t