case _ left =>
  apply Exists.intro hd.snd
  tauto
Node : Type
inst✝ : DecidableEq Node
hd : Node × List Node
tl : List (Node × List Node)
ih : ∀ (x y : Node), y ∈ direct_succ_list tl x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ tl
y : Node
left : y ∈ hd.2
⊢ ∃ ys, y ∈ ys ∧ ((hd.1, ys) = hd ∨ (hd.1, ys) ∈ tl)
no goals