no goals
V : Type u
inst✝ : Quiver V
a✝¹ b✝¹ c✝ d a b c x✝ : V
p : Path a b
q : Path b c
b✝ : V
r : Path c b✝
a✝ : b✝ ⟶ x✝
⊢ comp (comp p q) (cons r a✝) = comp p (comp q (cons r a✝))
rw [comp_cons, comp_cons, comp_cons, comp_assoc p q r]