{P : Sort u} →
  {steps : ℕ} →
    {infos : Lean.SubExpr.PosMap Lean.Elab.Info} →
      {holeIter : Lean.PrettyPrinter.Delaborator.SubExpr.HoleIterator} →
        {steps' : ℕ} →
          {infos' : Lean.SubExpr.PosMap Lean.Elab.Info} →
            {holeIter' : Lean.PrettyPrinter.Delaborator.SubExpr.HoleIterator} →
              { steps := steps, infos := infos, holeIter := holeIter } =
                  { steps := steps', infos := infos', holeIter := holeIter' } →
                (steps = steps' → infos = infos' → holeIter = holeIter' → P) → P