simp only [direct_succ_list]
Node : Type
inst✝ : DecidableEq Node
⊢ ∀ (x y : Node), y ∈ direct_succ_list [] x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ []
Node : Type
inst✝ : DecidableEq Node
⊢ ∀ (x y : Node), y ∈ [] ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ []