if hd : Descendant i k then
  have ⟨l, hl, _, hl'⟩ := h.exists_get_descendant k hk hd
  exact ⟨l, hl, hl'⟩
else
  simp only [h.get_not_descendant k hd]
  exact ⟨k, hk, rfl⟩
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
y : Subarray α
h : heapifyDown.OpSpec lt x i y
k : Nat
hk : k < Subarray.size x
⊢ ∃ l hl, y[k] = x[l]
no goals