{motive : Batteries.Random.MersenneTwister.Config → Sort u} →
  (t : Batteries.Random.MersenneTwister.Config) →
    ((wordSize stateSize : ℕ) →
        (shiftSize : Fin stateSize) →
          (maskBits : Fin wordSize) →
            (xorMask : BitVec wordSize) →
              (temperingShifts : ℕ × ℕ × ℕ × ℕ) →
                (temperingMasks : BitVec wordSize × BitVec wordSize × BitVec wordSize) →
                  (initMult initSeed : BitVec wordSize) →
                    motive
                      { wordSize := wordSize, stateSize := stateSize, shiftSize := shiftSize, maskBits := maskBits,
                        xorMask := xorMask, temperingShifts := temperingShifts, temperingMasks := temperingMasks,
                        initMult := initMult, initSeed := initSeed }) →
      motive t