refine Nat.foldRev_induction (motive:=fun n x => ∀ k, n ≤ k → IsHeap lt x k) _ _ x ?_ ?_ 0 .refl
α : 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
case refine_1
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
⊢ (fun n x => ∀ (k : Nat), n ≤ k → IsHeap lt x k) (Subarray.size x / 2) x

case refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
⊢ ∀ (k : Nat) (a : Subarray α),
    (fun n x => ∀ (k : Nat), n ≤ k → IsHeap lt x k) (k + 1) a →
      (fun n x => ∀ (k : Nat), n ≤ k → IsHeap lt x k) k (heapifyDown lt a k)