{R : Type u_5} →
  {E : Type u_6} →
    {F : Type u_7} →
      [inst : Add E] →
        [inst_1 : Add F] →
          [inst_2 : SMul R E] →
            [inst_3 : SMul R F] →
              {motive : FourierInvModule R E F → Sort u} →
                ((toFourierTransformInv : FourierTransformInv E F) →
                    (fourierInv_add :
                        ∀ (f g : E),
                          FourierTransformInv.fourierInv (f + g) =
                            FourierTransformInv.fourierInv f + FourierTransformInv.fourierInv g) →
                      (fourierInv_smul :
                          ∀ (r : R) (f : E),
                            FourierTransformInv.fourierInv (r • f) = r • FourierTransformInv.fourierInv f) →
                        motive
                          { toFourierTransformInv := toFourierTransformInv, fourierInv_add := fourierInv_add,
                            fourierInv_smul := fourierInv_smul }) →
                  (t : FourierInvModule R E F) → motive t