split_ifs
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
⊢ (y ∈ if hd.1 = x then hd.2 ++ direct_succ_list tl x else direct_succ_list tl x) ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ hd :: tl
case pos
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
h✝ : hd.1 = x
⊢ y ∈ hd.2 ++ direct_succ_list tl x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ hd :: tl

case neg
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
h✝ : ¬hd.1 = x
⊢ y ∈ direct_succ_list tl x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ hd :: tl