∀ {α : Type u_1} [inst : DecidableEq α] {p : α → Prop} {f : Equiv.Perm (Subtype p)} (motive : f.IsSwap → Prop)
  (h : f.IsSwap),
  (∀ (x : α) (hx : p x) (y : α) (hy : p y) (hxy : ⟨x, hx⟩ ≠ ⟨y, hy⟩ ∧ f = Equiv.swap ⟨x, hx⟩ ⟨y, hy⟩), motive ⋯) →
    motive h