U : Type u_1
inst✝ : Quiver U
u' v' : U
e : u' ⟶ v'
⊢ HEq (cast (_ : u' = u') (_ : v' = v') e) e
U : Type u_1
inst✝ : Quiver U
u v u' v' : U
hu : u = u'
hv : v = v'
e : u ⟶ v
⊢ HEq (cast hu hv e) e
subst_vars
no goals
U : Type u_1
inst✝ : Quiver U
u' v' : U
e : u' ⟶ v'
⊢ HEq (cast (_ : u' = u') (_ : v' = v') e) e
rfl