simp only [list_direct_succ_set]
case h1
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
stack : List Node
⊢ list_direct_succ_set g [] ⊆ ↑stack.toFinset ∪ ↑[].toFinset
case h1
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
stack : List Node
⊢ {y | ∃ x ∈ [], ∃ ys, y ∈ ys ∧ (x, ys) ∈ g} ⊆ ↑stack.toFinset ∪ ↑[].toFinset