case cons ih => simp [append]; apply ih
V : Sort u_1
inst✝ : Quiver V
A B C D : V
r : Path C D
A✝ B✝ C✝ : V
a✝¹ : A✝ ⟶ B✝
a✝ : Path B✝ C✝
ih : ∀ (q : Path C✝ C), append (append a✝ q) r = append a✝ (append q r)
q : Path C✝ C
⊢ append (append (cons a✝¹ a✝) q) r = append (cons a✝¹ a✝) (append q r)
no goals