induction p generalizing u with
| nil => exact ⟨_, nil, h, rfl⟩
| cons h' p ih =>
  obtain ⟨y, q, h'', hc⟩ := ih h'
  refine' ⟨y, cons h q, h'', _⟩
  rw [concat_cons, hc]
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v w : V
h : G.Adj u v
p : Walk G v w
⊢ ∃ x q h', cons h p = concat q h'
no goals