{C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {X Y : C} →
        {motive : CategoryTheory.ExactPairing X Y → Sort u} →
          ((coevaluation' :
                CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶
                  CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) →
              (evaluation' :
                  CategoryTheory.MonoidalCategoryStruct.tensorObj Y X ⟶
                    CategoryTheory.MonoidalCategoryStruct.tensorUnit C) →
                (coevaluation_evaluation' :
                    CategoryTheory.CategoryStruct.comp
                        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y coevaluation')
                        (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator Y X Y).inv
                          (CategoryTheory.MonoidalCategoryStruct.whiskerRight evaluation' Y)) =
                      CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor Y).hom
                        (CategoryTheory.MonoidalCategoryStruct.leftUnitor Y).inv) →
                  (evaluation_coevaluation' :
                      CategoryTheory.CategoryStruct.comp
                          (CategoryTheory.MonoidalCategoryStruct.whiskerRight coevaluation' X)
                          (CategoryTheory.CategoryStruct.comp
                            (CategoryTheory.MonoidalCategoryStruct.associator X Y X).hom
                            (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X evaluation')) =
                        CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom
                          (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).inv) →
                    motive
                      { coevaluation' := coevaluation', evaluation' := evaluation',
                        coevaluation_evaluation' := coevaluation_evaluation',
                        evaluation_coevaluation' := evaluation_coevaluation' }) →
            (t : CategoryTheory.ExactPairing X Y) → motive t