(motive : Aesop.NormalizationState → Sort u_1) →
  (x : Aesop.NormalizationState) →
    ((postState : Lean.Meta.SavedState) →
        (script : Array (Aesop.DisplayRuleName × Option (Array Aesop.Script.LazyStep))) →
          motive (Aesop.NormalizationState.provenByNormalization postState script)) →
      ((postGoal : Lean.MVarId) →
          (postState : Lean.Meta.SavedState) →
            (script : Array (Aesop.DisplayRuleName × Option (Array Aesop.Script.LazyStep))) →
              motive (Aesop.NormalizationState.normal postGoal postState script)) →
        (Unit → motive Aesop.NormalizationState.notNormal) → motive x