apply reachable_from_list.step y (x, ys) a2_right a2_left
Node : Type
x✝ : DecidableEq Node
g : Graph Node
x a y : Node
s1 : y ∈ direct_succ_list g x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ g
ih : ∃ ys, y ∈ ys ∧ (x, ys) ∈ g
ys : List Node
a2_left : y ∈ ys
a2_right : (x, ys) ∈ g
⊢ y ∈ reachable_from_list g [x]
Node : Type
x✝ : DecidableEq Node
g : Graph Node
x a y : Node
s1 : y ∈ direct_succ_list g x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ g
ih : ∃ ys, y ∈ ys ∧ (x, ys) ∈ g
ys : List Node
a2_left : y ∈ ys
a2_right : (x, ys) ∈ g
⊢ reachable_from_list g [x] (x, ys).1