∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : Cᵒᵖ} {f : X ⟶ Y} {g : Y ⟶ Z} {Z' : C}
  {h : Opposite.unop X ⟶ Z'},
  CategoryTheory.CategoryStruct.comp g.unop (CategoryTheory.CategoryStruct.comp f.unop h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g).unop h