rw [IH, start_heapifyDown]
case succ
α : Type u
lt : α → α → Bool
n : Nat
IH : ∀ (x : Subarray α), (mkHeap.loop lt x n).start = x.start
x : Subarray α
⊢ (mkHeap.loop lt (heapifyDown lt x n) n).start = x.start
no goals