intro
case mpr
V : Sort u_1
inst✝ : Quiver V
A✝ B C D A B✝ : V
a✝ : A ⟶ B✝
p : Path B✝ A
⊢ cons a✝ p = nil' A → length (cons a✝ p) = Nat.zero
case mpr
V : Sort u_1
inst✝ : Quiver V
A✝ B C D A B✝ : V
a✝¹ : A ⟶ B✝
p : Path B✝ A
a✝ : cons a✝¹ p = nil' A
⊢ length (cons a✝¹ p) = Nat.zero