induction n generalizing x with
| zero => rfl
| succ n IH => simp only [mkHeap.loop, IH, size_as_heapifyDown]
α : Type u
lt : α → α → Bool
x : Subarray α
n : Nat
⊢ Array.size (mkHeap.loop lt x n).as = Array.size x.as
no goals