case base a ih =>
  apply reachable_from_list.base
  apply Set.mem_of_subset_of_mem h1 ih
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
xs ys : List Node
h1 : xs ⊆ ys
x a : Node
ih : a ∈ xs
⊢ a ∈ reachable_from_list g ys
no goals