rewrite [mkHeap_eq_foldRev]
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
⊢ IsHeap lt (mkHeap lt x) 0
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
⊢ IsHeap lt (Nat.foldRev (fun n x => heapifyDown lt x n) (Subarray.size x / 2) x) 0