(R : Type u_5) →
  (E : Type u_6) →
    (F : outParam (Type u_7)) →
      {inst : Add E} →
        {inst_1 : Add F} →
          {inst_2 : SMul R E} →
            {inst_3 : SMul R F} → [SizeOf R] → [SizeOf E] → [SizeOf F] → SizeOf (FourierInvModule R E F)