∀ {α : Type u_1} {p : Finset α → Prop} (motive : (∃ s, ∃ (hs : s.Finite), p hs.toFinset) → Prop)
  (x : ∃ s, ∃ (hs : s.Finite), p hs.toFinset),
  (∀ (s : Set α) (hs : s.Finite) (hs' : p hs.toFinset), motive ⋯) → motive x