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
c1 : x ∈ ys
⊢ x ∈ reachable_from_list g xs ∨ x ∈ reachable_from_list g ys
no goals