{P : Sort u} →
  {numInst maxSize numRetries : ℕ} →
    {traceDiscarded traceSuccesses traceShrink traceShrinkCandidates : Bool} →
      {randomSeed : Option ℕ} →
        {quiet : Bool} →
          {numInst' maxSize' numRetries' : ℕ} →
            {traceDiscarded' traceSuccesses' traceShrink' traceShrinkCandidates' : Bool} →
              {randomSeed' : Option ℕ} →
                {quiet' : Bool} →
                  { numInst := numInst, maxSize := maxSize, numRetries := numRetries, traceDiscarded := traceDiscarded,
                        traceSuccesses := traceSuccesses, traceShrink := traceShrink,
                        traceShrinkCandidates := traceShrinkCandidates, randomSeed := randomSeed, quiet := quiet } =
                      { numInst := numInst', maxSize := maxSize', numRetries := numRetries',
                        traceDiscarded := traceDiscarded', traceSuccesses := traceSuccesses',
                        traceShrink := traceShrink', traceShrinkCandidates := traceShrinkCandidates',
                        randomSeed := randomSeed', quiet := quiet' } →
                    (numInst = numInst' →
                        maxSize = maxSize' →
                          numRetries = numRetries' →
                            traceDiscarded = traceDiscarded' →
                              traceSuccesses = traceSuccesses' →
                                traceShrink = traceShrink' →
                                  traceShrinkCandidates = traceShrinkCandidates' →
                                    randomSeed = randomSeed' → quiet = quiet' → P) →
                      P