induction hd with
| refl => exact h
| node_left j _ IH => exact IH h.left
| node_right j _ IH => exact IH h.right
α : Type u
lt : α → α → Bool
x : Subarray α
i j : Nat
h : IsHeap lt x i
hd : Descendant i j
⊢ IsHeap lt x j
no goals