{motive : Aesop.Options → Sort u} →
  (t : Aesop.Options) →
    ((strategy : Aesop.Strategy) →
        (maxRuleApplicationDepth maxRuleApplications maxGoals maxNormIterations maxSafePrefixRuleApplications : ℕ) →
          (applyHypsTransparency assumptionTransparency destructProductsTransparency : Lean.Meta.TransparencyMode) →
            (introsTransparency? : Option Lean.Meta.TransparencyMode) →
              (terminal warnOnNonterminal traceScript enableSimp useSimpAll useDefaultSimpSet enableUnfold : Bool) →
                motive
                  { strategy := strategy, maxRuleApplicationDepth := maxRuleApplicationDepth,
                    maxRuleApplications := maxRuleApplications, maxGoals := maxGoals,
                    maxNormIterations := maxNormIterations,
                    maxSafePrefixRuleApplications := maxSafePrefixRuleApplications,
                    applyHypsTransparency := applyHypsTransparency, assumptionTransparency := assumptionTransparency,
                    destructProductsTransparency := destructProductsTransparency,
                    introsTransparency? := introsTransparency?, terminal := terminal,
                    warnOnNonterminal := warnOnNonterminal, traceScript := traceScript, enableSimp := enableSimp,
                    useSimpAll := useSimpAll, useDefaultSimpSet := useDefaultSimpSet, enableUnfold := enableUnfold }) →
      motive t