∀ {α : Type u_1} {n : ℕ} {p : Finset α → Sort u_4}
  (H : (t₁ : Finset α) → ({t₂ : Finset α} → t₂.card ≤ n → t₁ ⊂ t₂ → p t₂) → t₁.card ≤ n → p t₁) (s : Finset α),
  Finset.strongDownwardInduction H s = H s fun {t} ht x => Finset.strongDownwardInduction H t ht