simp only [s1] at ih
Node : Type
x✝ : DecidableEq Node
g : Graph Node
x a y : Node
ih : y ∈ direct_succ_list g x
s1 : y ∈ direct_succ_list g x ↔ ∃ ys, y ∈ ys ∧ (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
⊢ y ∈ reachable_from_list g [x]