induction p
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
inst✝ : DecidableEq V
u v w : V
p : Walk G v w
h : u ∈ support p
⊢ append (takeUntil p u h) (dropUntil p u h) = p
case nil
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
inst✝ : DecidableEq V
u v w u✝ : V
h : u ∈ support nil
⊢ append (takeUntil nil u h) (dropUntil nil u h) = nil

case cons
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
inst✝ : DecidableEq V
u v w u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : Walk G v✝ w✝
p_ih✝ : ∀ (h : u ∈ support p✝), append (takeUntil p✝ u h) (dropUntil p✝ u h) = p✝
h : u ∈ support (cons h✝ p✝)
⊢ append (takeUntil (cons h✝ p✝) u h) (dropUntil (cons h✝ p✝) u h) = cons h✝ p✝