α : Type u_1
β : Type ?u.82569
γ : Type ?u.82572
p : Multiset α → Sort u_2
s : Multiset α
n : ℕ
H : (t₁ : Multiset α) → ({t₂ : Multiset α} → ↑card t₂ ≤ n → t₁ < t₂ → p t₂) → ↑card t₁ ≤ n → p t₁
⊢ (fun a => strongDownwardInduction H s a) = H s fun {t} ht _h => strongDownwardInduction H t ht
α : Type u_1
β : Type ?u.82569
γ : Type ?u.82572
p : Multiset α → Sort u_2
s : Multiset α
n : ℕ
H : (t₁ : Multiset α) → ({t₂ : Multiset α} → ↑card t₂ ≤ n → t₁ < t₂ → p t₂) → ↑card t₁ ≤ n → p t₁
⊢ (fun a => strongDownwardInductionOn s H a) = H s fun {t} ht _h => strongDownwardInductionOn t H ht
dsimp only [strongDownwardInductionOn]
no goals
α : Type u_1
β : Type ?u.82569
γ : Type ?u.82572
p : Multiset α → Sort u_2
s : Multiset α
n : ℕ
H : (t₁ : Multiset α) → ({t₂ : Multiset α} → ↑card t₂ ≤ n → t₁ < t₂ → p t₂) → ↑card t₁ ≤ n → p t₁
⊢ (fun a => strongDownwardInduction H s a) = H s fun {t} ht _h => strongDownwardInduction H t ht
rw [strongDownwardInduction]