intro zs a2
case mpr
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
a1 : ∃ ys, y ∈ ys ∧ (ys = hd.2 ∨ (hd.1, ys) ∈ tl)
⊢ ∀ (a : List Node), y ∈ a ∧ (a = hd.2 ∨ (hd.1, a) ∈ tl) → y ∈ hd.2 ∨ ∃ ys, y ∈ ys ∧ (hd.1, ys) ∈ tl
case mpr
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
a1 : ∃ ys, y ∈ ys ∧ (ys = hd.2 ∨ (hd.1, ys) ∈ tl)
zs : List Node
a2 : y ∈ zs ∧ (zs = hd.2 ∨ (hd.1, zs) ∈ tl)
⊢ y ∈ hd.2 ∨ ∃ ys, y ∈ ys ∧ (hd.1, ys) ∈ tl