no goals
α : Type u_1
β : Type ?u.74113
s✝ t : Finset α
f : α → β
n : ℕ
p : Finset α → Sort u_2
H : (s : Finset α) → ((t : Finset α) → t ⊂ s → p t) → p s
s : Finset α
⊢ strongInduction H s = H s fun t x => strongInduction H t
rw [strongInduction]