{P : Sort u} →
  {localInsts : Lean.LocalInstances} →
    {type : Lean.Expr} →
      {synthPendingDepth : ℕ} →
        {localInsts' : Lean.LocalInstances} →
          {type' : Lean.Expr} →
            {synthPendingDepth' : ℕ} →
              { localInsts := localInsts, type := type, synthPendingDepth := synthPendingDepth } =
                  { localInsts := localInsts', type := type', synthPendingDepth := synthPendingDepth' } →
                (localInsts = localInsts' → type = type' → synthPendingDepth = synthPendingDepth' → P) → P