exact ⟨k,hk,hdesc,rfl⟩
case leaf
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
y : Subarray α
k : Nat
x✝ : Subarray α
i✝ : Nat
a✝ : 2 * i✝ + 1 ≥ Subarray.size x✝
hk : k < Subarray.size x✝
hdesc : Descendant i✝ k
⊢ ∃ l hl, Descendant i✝ l ∧ x✝[k] = x✝[l]
no goals