theorem reverse_cons_length {V : Type} {G : SimpleGraph V} (a v₀ w : V) (p' : G.Walk a w) (p : G.Walk v₀ w) (h : G.Adj v₀ a) {k : ℕ} (hp : p.length = k.succ) (hp' : p = SimpleGraph.Walk.cons h p') : p'.length = k

theorem vertex_in_walk_induction {V : Type} {G : SimpleGraph V} {S : Set V} {w : V} (hw : w ∉ S) (n : ℕ) (t : V) : t ∈ S → ∀ (p : G.Walk t w), p.length = n → ∃ (a : V), ∃ u ∈ S, G.Adj u a ∧ a ∉ S

theorem vertex_in_walk {V : Type} {G : SimpleGraph V} (S : Set V) (w t : V) (hw : w ∉ S) (ht : t ∈ S) (p : G.Walk t w) : ∃ (a : V), ∃ u ∈ S, G.Adj u a ∧ a ∉ S