∀ {V : Type u_2} [inst : Quiver V] (v : V),
  (∀ (w : V), Quiver.StronglyConnectedComponent.mk w = Quiver.StronglyConnectedComponent.mk v → w = v) ↔
    ∀ (w : V), w ≠ v → ¬(Nonempty (Quiver.Path v w) ∧ Nonempty (Quiver.Path w v))