simp only [h.get_not_descendant k hd]
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
y : Subarray α
h : heapifyDown.OpSpec lt x i y
k : Nat
hk : k < Subarray.size x
hd : ¬Descendant i k
⊢ ∃ l hl, y[k] = x[l]
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
y : Subarray α
h : heapifyDown.OpSpec lt x i y
k : Nat
hk : k < Subarray.size x
hd : ¬Descendant i k
⊢ ∃ l hl, x[k] = x[l]