dsimp [mkHeap.loop]
case succ
α : Type u
lt : α → α → Bool
n : Nat
IH : ∀ (x : Subarray α), (mkHeap.loop lt x n).stop = x.stop
x : Subarray α
⊢ (mkHeap.loop lt x (Nat.succ n)).stop = x.stop
case succ
α : Type u
lt : α → α → Bool
n : Nat
IH : ∀ (x : Subarray α), (mkHeap.loop lt x n).stop = x.stop
x : Subarray α
⊢ (mkHeap.loop lt (heapifyDown lt x n) n).stop = x.stop