apply reachable_from_list.base
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
case a
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
xs ys : List Node
h1 : xs ⊆ ys
x a : Node
ih : a ∈ xs
⊢ a ∈ ys