case cons hd tl ih =>
  simp only [list_direct_succ_list_cons] at a1
  simp only [reachable_from_list_of_cons g hd tl]
  simp
  simp only [reachable_from_list_of_append] at a1
  simp at a1
  cases a1
  case _ left =>
    left
    obtain s1 := reachable_from_list_direct_succ_list_is_subset_of_reachable_from_list g hd
    exact Set.mem_of_subset_of_mem s1 left
  case _ right =>
    right
    exact ih right
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
x hd : Node
tl : List Node
ih : x ∈ reachable_from_list g (list_direct_succ_list g tl) → x ∈ reachable_from_list g tl
a1 : x ∈ reachable_from_list g (list_direct_succ_list g (hd :: tl))
⊢ x ∈ reachable_from_list g (hd :: tl)
no goals