induction a1
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
x a : Node
a1 : a ∈ reachable_from_list g (direct_succ_list g x)
⊢ a ∈ reachable_from_list g [x]
case base
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
x a x✝ : Node
a✝ : x✝ ∈ direct_succ_list g x
⊢ x✝ ∈ reachable_from_list g [x]

case step
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
x a x✝ : Node
e✝ : Node × List Node
a✝² : e✝ ∈ g
a✝¹ : x✝ ∈ e✝.2
a✝ : reachable_from_list g (direct_succ_list g x) e✝.1
a_ih✝ : e✝.1 ∈ reachable_from_list g [x]
⊢ x✝ ∈ reachable_from_list g [x]