let _hy_left := fun hl => h.not_lt_left hl heap_left
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
i : Nat
y : Subarray α
h : heapifyDown.OpSpec lt x i y
heap_left : IsHeap lt x (2 * i + 1)
heap_right : IsHeap lt x (2 * i + 2)
⊢ IsHeap lt y i
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
i : Nat
y : Subarray α
h : heapifyDown.OpSpec lt x i y
heap_left : IsHeap lt x (2 * i + 1)
heap_right : IsHeap lt x (2 * i + 2)
_hy_left : ∀ (hl : 2 * i + 1 < Subarray.size x), lt y[i] y[2 * i + 1] = false := fun hl => not_lt_left h hl heap_left
⊢ IsHeap lt y i