case _ x e ih_1 ih_2 ih_3 ih_4 =>
  cases ih_4
  case _ left =>
    left
    exact reachable_from_list.step x e ih_1 ih_2 left
  case _ right =>
    right
    exact reachable_from_list.step x e ih_1 ih_2 right
Node : Type
inst : DecidableEq Node
g : Graph Node
xs ys : List Node
x✝ x : Node
e : Node × List Node
ih_1 : e ∈ g
ih_2 : x ∈ e.2
ih_3 : reachable_from_list g (xs ++ ys) e.1
ih_4 : e.1 ∈ reachable_from_list g xs ∨ e.1 ∈ reachable_from_list g ys
⊢ x ∈ reachable_from_list g xs ∨ x ∈ reachable_from_list g ys
no goals