rw [concat_cons, hc]
case cons.intro.intro.intro
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
v w u✝ v✝ w✝ : V
h' : G.Adj u✝ v✝
p : Walk G v✝ w✝
ih : ∀ {u : V} (h : G.Adj u v✝), ∃ x q h', cons h p = concat q h'
u : V
h : G.Adj u u✝
y : V
q : Walk G u✝ y
h'' : G.Adj y w✝
hc : cons h' p = concat q h''
⊢ cons h (cons h' p) = concat (cons h q) h''
no goals