{motive : BoxIntegral.IntegrationParams → Sort u} →
  (t : BoxIntegral.IntegrationParams) →
    ((bRiemann bHenstock bDistortion : Bool) →
        motive { bRiemann := bRiemann, bHenstock := bHenstock, bDistortion := bDistortion }) →
      motive t