rewrite [h]
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
stop : Nat
h✝ : Algdata.BinaryHeap.heapSort.Intermed lt x stop
i k : Nat
hi : (BinaryHeap.popMax lt x).stop ≤ i ∧ i < stop
hk : k < Subarray.size (BinaryHeap.popMax lt x)
k' : Nat
hk' : k' < Subarray.size x
left✝ : 0 < k'
h : (BinaryHeap.popMax lt x)[k] = x[k']
⊢ lt (BinaryHeap.popMax lt x).as[i] (BinaryHeap.popMax lt x)[k] = false
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
stop : Nat
h✝ : Algdata.BinaryHeap.heapSort.Intermed lt x stop
i k : Nat
hi : (BinaryHeap.popMax lt x).stop ≤ i ∧ i < stop
hk : k < Subarray.size (BinaryHeap.popMax lt x)
k' : Nat
hk' : k' < Subarray.size x
left✝ : 0 < k'
h : (BinaryHeap.popMax lt x)[k] = x[k']
⊢ lt (BinaryHeap.popMax lt x).as[i] x[k'] = false