rw [Nat.succ_add]
V : Sort u_1
inst✝ : Quiver V
A✝ B✝² C✝ D A B✝¹ C B B✝ : V
a✝ : A ⟶ B✝
p' : Path B✝ B
q : Path B C
⊢ Nat.succ (length (append p' q)) = Nat.succ (length p') + length q
V : Sort u_1
inst✝ : Quiver V
A✝ B✝² C✝ D A B✝¹ C B B✝ : V
a✝ : A ⟶ B✝
p' : Path B✝ B
q : Path B C
⊢ Nat.succ (length (append p' q)) = Nat.succ (length p' + length q)