simp at a1
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
xs : List Node
x : Node
a1 : x ∈ ↑xs.toFinset
⊢ x ∈ reachable_from_list g xs
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
xs : List Node
x : Node
a1 : x ∈ xs
⊢ x ∈ reachable_from_list g xs