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

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