specialize IH₂ fun k hk h => hext k hk (.node_right _ h)
case node'
α : Type u
lt : α → α → Bool
x y : Subarray α
i✝ : Nat
hsize : Subarray.size y ≤ Subarray.size x
i : Nat
x✝ : i < Subarray.size x
lt_left : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
lt_right : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
IH₂ : (∀ (k : Nat) (hk : k < Subarray.size y), Descendant (2 * i + 2) k → y[k] = x[k]) → IsHeap lt y (2 * i + 2)
hext : ∀ (k : Nat) (hk : k < Subarray.size y), Descendant i k → y[k] = x[k]
IH₁ : IsHeap lt y (2 * i + 1)
⊢ IsHeap lt y i
case node'
α : Type u
lt : α → α → Bool
x y : Subarray α
i✝ : Nat
hsize : Subarray.size y ≤ Subarray.size x
i : Nat
x✝ : i < Subarray.size x
lt_left : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
lt_right : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hext : ∀ (k : Nat) (hk : k < Subarray.size y), Descendant i k → y[k] = x[k]
IH₁ : IsHeap lt y (2 * i + 1)
IH₂ : IsHeap lt y (2 * i + 2)
⊢ IsHeap lt y i