∀ {V : Type u} [inst : Quiver V] {a b c : V} (a_1 : Quiver.Path a b) (a_2 : b ⟶ c) (b_1 : V) (a_3 : Quiver.Path a b_1)
  (a_4 : b_1 ⟶ c), (a_1.cons a_2 = a_3.cons a_4) = (b = b_1 ∧ a_1 ≍ a_3 ∧ a_2 ≍ a_4)