induction g
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
x : Node
h1 : x ∉ g.nodes_of
⊢ direct_succ_list g x = []
case nil
Node : Type
inst✝ : DecidableEq Node
x : Node
h1 : x ∉ Graph.nodes_of []
⊢ direct_succ_list [] x = []

case cons
Node : Type
inst✝ : DecidableEq Node
x : Node
head✝ : Node × List Node
tail✝ : List (Node × List Node)
tail_ih✝ : x ∉ Graph.nodes_of tail✝ → direct_succ_list tail✝ x = []
h1 : x ∉ Graph.nodes_of (head✝ :: tail✝)
⊢ direct_succ_list (head✝ :: tail✝) x = []