{P : Sort u} →
  {info : Lean.Lsp.RpcRef} →
    {subexprPos : String} →
      {diffStatus? : Option String} →
        {info' : Lean.Lsp.RpcRef} →
          {subexprPos' : String} →
            {diffStatus?' : Option String} →
              { info := info, subexprPos := subexprPos, diffStatus? := diffStatus? } =
                  { info := info', subexprPos := subexprPos', diffStatus? := diffStatus?' } →
                (info = info' → subexprPos = subexprPos' → diffStatus? = diffStatus?' → P) → P