∀ {V : Type u_2} [inst : Quiver V] (n : ℕ) (a x x_1 x_2 : V),
  ¬x_1 = x_2 →
    ∀ (p' : Quiver.Path a x_1) (α : x_1 ⟶ x) (q' : Quiver.Path a x_2) (β : x_2 ⟶ x) (hp : (p'.cons α).length ≤ n + 1)
      (hq : (q'.cons β).length ≤ n + 1), ⟨p'.cons α, hp⟩ = ⟨q'.cons β, hq⟩ → False