intro ⟨s, h1, h2⟩
case mpr
α : Type
inst✝ : DecidableEq α
g : Graph α
S : List α
s' : α
⊢ (∃ s ∈ S, Relation.ReflTransGen (fun a b => ∃ l, (a, l) ∈ g ∧ b ∈ l) s s') → s' ∈ reachable_from_list g S
case mpr
α : Type
inst✝ : DecidableEq α
g : Graph α
S : List α
s' s : α
h1 : s ∈ S
h2 : Relation.ReflTransGen (fun a b => ∃ l, (a, l) ∈ g ∧ b ∈ l) s s'
⊢ s' ∈ reachable_from_list g S