∀ {α : Type u_1} {w₁ w₂ : α} {s t : Finset α} [inst : DecidableEq α] (W : Finset α)
  (motive : insert w₁ s ⊆ W ∧ insert w₂ t ⊆ W → Prop) (x : insert w₁ s ⊆ W ∧ insert w₂ t ⊆ W),
  (∀ (h1s : insert w₁ s ⊆ W) (h2t : insert w₂ t ⊆ W), motive ⋯) → motive x