induction h with
| base _ h => exact ⟨_, h, .refl⟩
| step _ _ h1 h2 _ ih =>
  have ⟨_, h3, h4⟩ := ih
  exact ⟨_, h3, .tail h4 ⟨_, h1, h2⟩⟩
case mp
α : Type
inst✝ : DecidableEq α
g : Graph α
S : List α
s' : α
h : s' ∈ reachable_from_list g S
⊢ ∃ s ∈ S, Relation.ReflTransGen (fun a b => ∃ l, (a, l) ∈ g ∧ b ∈ l) s s'
no goals