apply reachable_from_list_mono g ys (xs ++ ys)
Node : Type
inst : DecidableEq Node
g : Graph Node
xs ys : List Node
x : Node
right : x ∈ reachable_from_list g ys
⊢ x ∈ reachable_from_list g (xs ++ ys)
case h1
Node : Type
inst : DecidableEq Node
g : Graph Node
xs ys : List Node
x : Node
right : x ∈ reachable_from_list g ys
⊢ ys ⊆ xs ++ ys

case a
Node : Type
inst : DecidableEq Node
g : Graph Node
xs ys : List Node
x : Node
right : x ∈ reachable_from_list g ys
⊢ x ∈ reachable_from_list g ys