cases a2
case mp
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
x y : Node
c1 : ¬hd.1 = x
a1 : ∃ ys, y ∈ ys ∧ (x, ys) ∈ tl
zs : List Node
a2 : y ∈ zs ∧ (x, zs) ∈ tl
⊢ ∃ ys, y ∈ ys ∧ ((x, ys) = hd ∨ (x, ys) ∈ tl)
case mp.intro
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
x y : Node
c1 : ¬hd.1 = x
a1 : ∃ ys, y ∈ ys ∧ (x, ys) ∈ tl
zs : List Node
left✝ : y ∈ zs
right✝ : (x, zs) ∈ tl
⊢ ∃ ys, y ∈ ys ∧ ((x, ys) = hd ∨ (x, ys) ∈ tl)