simp
Node : Type
x✝ : DecidableEq Node
g : Graph Node
x a y : Node
s1 : y ∈ direct_succ_list g x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ g
ih : ∃ ys, y ∈ ys ∧ (x, ys) ∈ g
ys : List Node
a2_left : y ∈ ys
a2_right : (x, ys) ∈ g
⊢ x ∈ [x]
no goals