simp only [Graph.nodes_of] at ih
Node : Type
inst✝ : DecidableEq Node
x : Node
hd : Node × List Node
tl : List (Node × List Node)
ih : x ∉ Graph.nodes_of tl → direct_succ_list tl x = []
h1 : x ∉ Graph.nodes_of (hd :: tl)
⊢ direct_succ_list (hd :: tl) x = []
Node : Type
inst✝ : DecidableEq Node
x : Node
hd : Node × List Node
tl : List (Node × List Node)
ih : x ∉ List.map Prod.fst tl ∪ (List.map Prod.snd tl).join → direct_succ_list tl x = []
h1 : x ∉ Graph.nodes_of (hd :: tl)
⊢ direct_succ_list (hd :: tl) x = []