induction h2 with
| refl => exact reachable_from_list.base _ h1
| tail _ h ih =>
  have ⟨_, h3, h4⟩ := h
  exact reachable_from_list.step _ _ h3 h4 ih
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
no goals