show ∀ (n : Nat) (x : Subarray α), (∀ k, n+1 ≤ k → IsHeap lt x k) → ∀ k, n ≤ k → IsHeap lt (heapifyDown lt x n) k
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)
case refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
⊢ ∀ (n : Nat) (x : Subarray α),
    (∀ (k : Nat), n + 1 ≤ k → IsHeap lt x k) → ∀ (k : Nat), n ≤ k → IsHeap lt (heapifyDown lt x n) k