{P : Sort u} →
  {localSorryMap : Lean.NameMap Lean.Name} →
    {modified : Bool} →
      {localSorryMap' : Lean.NameMap Lean.Name} →
        {modified' : Bool} →
          { localSorryMap := localSorryMap, modified := modified } =
              { localSorryMap := localSorryMap', modified := modified' } →
            (localSorryMap = localSorryMap' → modified = modified' → P) → P