specialize @IH (heapifyDown lt x n)
  ((size_as_mkHeap_loop lt _ n).symm ▸ size_as_heapifyDown lt x n ▸ hk)
  (stop_heapifyDown lt x n ▸ hge)
case succ
α : Type u
lt : α → α → Bool
k n : Nat
IH : ∀ (x : Subarray α) {hk : k < Array.size (mkHeap.loop lt x n).as}, k ≥ x.stop → (mkHeap.loop lt x n).as[k] = x.as[k]
x : Subarray α
hk✝ : k < Array.size (mkHeap.loop lt (heapifyDown lt x n) n).as
hk : k < Array.size x.as
hge : k ≥ x.stop
⊢ (mkHeap.loop lt (heapifyDown lt x n) n).as[k] = x.as[k]
case succ
α : Type u
lt : α → α → Bool
k n : Nat
x : Subarray α
hk✝ : k < Array.size (mkHeap.loop lt (heapifyDown lt x n) n).as
hk : k < Array.size x.as
hge : k ≥ x.stop
IH : (mkHeap.loop lt (heapifyDown lt x n) n).as[k] = (heapifyDown lt x n).as[k]
⊢ (mkHeap.loop lt (heapifyDown lt x n) n).as[k] = x.as[k]