rw [snoc_cons, snoc, last, ← snoc_cons]
V : Sort u_1
inst✝ : Quiver V
A B C D x✝³ x✝² x✝¹ B✝¹ : V
a✝² : x✝³ ⟶ B✝¹
B✝ : V
a✝¹ : B✝¹ ⟶ B✝
a✝ : Path B✝ x✝²
x✝ : x✝² ⟶ x✝¹
⊢ last (snoc (cons' x✝³ B✝¹ x✝² a✝² (cons a✝¹ a✝)) x✝) = x✝²
V : Sort u_1
inst✝ : Quiver V
A B C D x✝³ x✝² x✝¹ B✝¹ : V
a✝² : x✝³ ⟶ B✝¹
B✝ : V
a✝¹ : B✝¹ ⟶ B✝
a✝ : Path B✝ x✝²
x✝ : x✝² ⟶ x✝¹
⊢ last (snoc (cons a✝¹ a✝) x✝) = x✝²