case refl
C : Type u₁
inst✝ : Category C
X : Cᵒᵖ
⊢ (eqToHom (_ : X = X)).unop = eqToHom (_ : X.unop = X.unop)
C : Type u₁
inst✝ : Category C
X Y : Cᵒᵖ
h : X = Y
⊢ (eqToHom h).unop = eqToHom (_ : Y.unop = X.unop)
cases h
no goals
case refl
C : Type u₁
inst✝ : Category C
X : Cᵒᵖ
⊢ (eqToHom (_ : X = X)).unop = eqToHom (_ : X.unop = X.unop)
rfl