case nil
U : Type u_1
inst✝ : Quiver U
u : U
hzero : length nil = 0
⊢ Path.cast (_ : u = u) (_ : u = u) nil = nil
U : Type u_1
inst✝ : Quiver U
u v : U
p : Path u v
hzero : length p = 0
⊢ Path.cast (_ : u = v) (_ : v = v) p = nil
cases p <;> simp only [Nat.succ_ne_zero, length_cons] at hzero
no goals
case nil
U : Type u_1
inst✝ : Quiver U
u : U
hzero : length nil = 0
⊢ Path.cast (_ : u = u) (_ : u = u) nil = nil
rfl