U : Type u_1
inst✝ : Quiver U
u' : U
⊢ cast (_ : u' = u') (_ : u' = u') nil = nil
U : Type u_1
inst✝ : Quiver U
u u' : U
hu : u = u'
⊢ cast hu hu nil = nil
subst_vars
no goals
U : Type u_1
inst✝ : Quiver U
u' : U
⊢ cast (_ : u' = u') (_ : u' = u') nil = nil
rfl