case _ x ih =>
  simp at ih
  cases ih
  case inl c1 =>
    left
    exact reachable_from_list.base x c1
  case inr c1 =>
    right
    exact reachable_from_list.base x c1
Node : Type
inst : DecidableEq Node
g : Graph Node
xs ys : List Node
x✝ x : Node
ih : x ∈ xs ++ ys
⊢ x ∈ reachable_from_list g xs ∨ x ∈ reachable_from_list g ys
no goals