Paths with at most one arrow between vertices

In a quiver with at most one arrow between any two vertices, a path is determined by its list of vertices. This is used to compare images of paths under automorphisms of trees.

theorem Quiver.Path.heq_of_vertices_eq {V : Type u_1} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] {a b : V} (p : Path a b) {a' b' : V} (q : Path a' b') : p.vertices = q.vertices → p ≍ q

theorem Quiver.Path.eq_cast_of_vertices_eq {V : Type u_1} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] {a b a' b' : V} (p : Path a b) (q : Path a' b') (ha : a' = a) (hb : b' = b) (h : p.vertices = q.vertices) : p = cast ha hb q