induction hij with
| refl => exact hjk
| node_left i _ IH => exact .node_left i IH
| node_right i _ IH => exact .node_right i IH
i j k : Nat
hij : Descendant i j
hjk : Descendant j k
⊢ Descendant i k
no goals