U : Type u_1
inst✝ : Quiver U
u v v' w : U
p : Path u v
p' : Path u v'
e : v ⟶ w
e' : v' ⟶ w
h : cons p e = cons p' e'
⊢ HEq p p'
U : Type u_1
inst✝ : Quiver U
u v v' w : U
p : Path u v
p' : Path u v'
e : v ⟶ w
e' : v' ⟶ w
h : cons p e = cons p' e'
⊢ Path.cast (_ : u = u) (_ : v = v') p = p'
rw [Path.cast_eq_iff_heq]
no goals
U : Type u_1
inst✝ : Quiver U
u v v' w : U
p : Path u v
p' : Path u v'
e : v ⟶ w
e' : v' ⟶ w
h : cons p e = cons p' e'
⊢ HEq p p'
exact heq_of_cons_eq_cons h