case neg c1 =>
  tauto
Node : Type
inst✝ : DecidableEq Node
x : Node
hd : Node × List Node
tl : List (Node × List Node)
ih :
  (∀ (x_1 : List Node), (x, x_1) ∉ tl) →
    (∀ (x_1 : List Node) (x_2 : Node), (x_2, x_1) ∈ tl → x ∉ x_1) → direct_succ_list tl x = []
h1 :
  ¬x = hd.1 ∧
    (∀ (x_1 : List Node), (x, x_1) ∉ tl) ∧ x ∉ hd.2 ∧ ∀ (x_1 : List Node) (x_2 : Node), (x_2, x_1) ∈ tl → x ∉ x_1
c1 : ¬hd.1 = x
⊢ direct_succ_list tl x = []
no goals