dsimp [append]
V : Sort u_1
inst✝ : Quiver V
A B C D : V
p' : Path C D
A✝ B✝ C✝ : V
a✝¹ : A✝ ⟶ B✝
a✝ : Path B✝ C✝
ih : ∀ (e : C✝ ⟶ C), append a✝ (cons e p') = append (snoc a✝ e) p'
e : C✝ ⟶ C
⊢ append (cons a✝¹ a✝) (cons e p') = append (snoc (cons a✝¹ a✝) e) p'
V : Sort u_1
inst✝ : Quiver V
A B C D : V
p' : Path C D
A✝ B✝ C✝ : V
a✝¹ : A✝ ⟶ B✝
a✝ : Path B✝ C✝
ih : ∀ (e : C✝ ⟶ C), append a✝ (cons e p') = append (snoc a✝ e) p'
e : C✝ ⟶ C
⊢ cons a✝¹ (append a✝ (cons e p')) = cons a✝¹ (append (snoc a✝ e) p')