∀ {α : Type u_2} {β : Type u_3} {γ : Type u_1} {f : α → β → γ} {s : Set α} {t : Set β}
  (motive : (Set.image2 f s t).Nonempty → Prop) (x : (Set.image2 f s t).Nonempty),
  (∀ (w : γ) (a : α) (ha : a ∈ s) (b : β) (hb : b ∈ t) (right : f a b = w), motive ⋯) → motive x