{motive : Aesop.RuleApplication → Sort u} →
  (t : Aesop.RuleApplication) →
    ((goals : Array Aesop.Subgoal) →
        (postState : Lean.Meta.SavedState) →
          (scriptSteps? : Option (Array Aesop.Script.LazyStep)) →
            (successProbability? : Option Aesop.Percent) →
              motive
                { goals := goals, postState := postState, scriptSteps? := scriptSteps?,
                  successProbability? := successProbability? }) →
      motive t