induction h with
| refl i => exact refl
| node_left i h IH =>
  exact node_left i h <| IH refl node_left node_right
| node_right i h IH =>
  exact node_right i h <| IH refl node_left node_right
k : Nat
motive : (i : Nat) → Descendant i k → Prop
i : Nat
h : Descendant i k
refl : motive k (_ : Descendant k k)
node_left : ∀ (i : Nat) (h : Descendant (2 * i + 1) k), motive (2 * i + 1) h → motive i (_ : Descendant i k)
node_right : ∀ (i : Nat) (h : Descendant (2 * i + 2) k), motive (2 * i + 2) h → motive i (_ : Descendant i k)
⊢ motive i h
no goals