{motive : Lean.Environment.Replay.State✝ → Sort u} →
  (t : Lean.Environment.Replay.State✝) →
    ((env : Lean.Kernel.Environment) →
        (remaining pending postponedConstructors postponedRecursors : Lean.NameSet) →
          motive
            { env := env, remaining := remaining, pending := pending, postponedConstructors := postponedConstructors,
              postponedRecursors := postponedRecursors }) →
      motive t