∀ {α : Type u} {motive : (s : Set α) → s.Finite → Prop} (s : Set α) (hs : s.Finite),
  motive ∅ ⋯ →
    (∀ {a : α} {t : Set α}, a ∈ s → ∀ (hts : t ⊆ s), a ∉ t → motive t ⋯ → motive (insert a t) ⋯) → motive s hs