case _ x y ih =>
  obtain s1 := mem_direct_succ_list_iff g x y
  simp only [s1] at ih
  apply Exists.elim ih
  intro ys a2
  cases a2
  case _ a2_left a2_right =>
    apply reachable_from_list.step y (x, ys) a2_right a2_left
    apply reachable_from_list.base x
    simp
Node : Type
x✝ : DecidableEq Node
g : Graph Node
x a y : Node
ih : y ∈ direct_succ_list g x
⊢ y ∈ reachable_from_list g [x]
no goals