{P : Sort u} →
  {postState : Lean.Meta.SavedState} →
    {script : Array (Aesop.DisplayRuleName × Option (Array Aesop.Script.LazyStep))} →
      {postState' : Lean.Meta.SavedState} →
        {script' : Array (Aesop.DisplayRuleName × Option (Array Aesop.Script.LazyStep))} →
          Aesop.NormalizationState.provenByNormalization postState script =
              Aesop.NormalizationState.provenByNormalization postState' script' →
            (postState = postState' → script = script' → P) → P