induction p with
| nil => rfl
| cons h p' ih =>
  dsimp only [append]
  rw [ih]
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v w x : V
p : Walk G u v
q : Walk G v w
r : Walk G w x
⊢ append p (append q r) = append (append p q) r
no goals