rw [Nat.add_comm]
V : Sort u_1
inst✝ : Quiver V
A✝ B✝ C✝ D A B C : V
q : Path A C
⊢ length (append nil q) = length nil + length q
V : Sort u_1
inst✝ : Quiver V
A✝ B✝ C✝ D A B C : V
q : Path A C
⊢ length (append nil q) = length q + length nil