cases a1
Node : Type
inst : DecidableEq Node
g : Graph Node
xs ys : List Node
x : Node
a1 : x ∈ reachable_from_list g xs ∨ x ∈ reachable_from_list g ys
⊢ x ∈ reachable_from_list g (xs ++ ys)
case inl
Node : Type
inst : DecidableEq Node
g : Graph Node
xs ys : List Node
x : Node
h✝ : x ∈ reachable_from_list g xs
⊢ x ∈ reachable_from_list g (xs ++ ys)

case inr
Node : Type
inst : DecidableEq Node
g : Graph Node
xs ys : List Node
x : Node
h✝ : x ∈ reachable_from_list g ys
⊢ x ∈ reachable_from_list g (xs ++ ys)