induction xs
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
xs : List Node
x : Node
a1 : x ∈ reachable_from_list g (list_direct_succ_list g xs)
⊢ x ∈ reachable_from_list g xs
case nil
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
x : Node
a1 : x ∈ reachable_from_list g (list_direct_succ_list g [])
⊢ x ∈ reachable_from_list g []

case cons
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
x head✝ : Node
tail✝ : List Node
tail_ih✝ : x ∈ reachable_from_list g (list_direct_succ_list g tail✝) → x ∈ reachable_from_list g tail✝
a1 : x ∈ reachable_from_list g (list_direct_succ_list g (head✝ :: tail✝))
⊢ x ∈ reachable_from_list g (head✝ :: tail✝)