{motive : Aesop.NormalizationState → Sort u} →
  (t : Aesop.NormalizationState) →
    motive Aesop.NormalizationState.notNormal →
      ((postGoal : Lean.MVarId) →
          (postState : Lean.Meta.SavedState) →
            (script : Array (Aesop.DisplayRuleName × Option (Array Aesop.Script.LazyStep))) →
              motive (Aesop.NormalizationState.normal postGoal postState script)) →
        ((postState : Lean.Meta.SavedState) →
            (script : Array (Aesop.DisplayRuleName × Option (Array Aesop.Script.LazyStep))) →
              motive (Aesop.NormalizationState.provenByNormalization postState script)) →
          motive t