case nil =>
  simp only [list_direct_succ_list] at a1
  simp at a1
  exact a1
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
x : Node
a1 : x ∈ reachable_from_list g (list_direct_succ_list g [])
⊢ x ∈ reachable_from_list g []
no goals