case cons hd tl ih =>
  simp only [Graph.nodes_of] at ih
  simp at ih
  simp only [Graph.nodes_of] at h1
  simp at h1
  simp only [direct_succ_list]
  split_ifs
  case pos c1 =>
    subst c1
    simp at h1
  case neg c1 =>
    tauto
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 = []
no goals