{P : Sort u} →
  {script script' : Array (Aesop.DisplayRuleName × Option (Array Aesop.Script.LazyStep))} →
    Aesop.NormSeqResult.proved script = Aesop.NormSeqResult.proved script' → (script = script' → P) → P