{P : Sort u} →
  {role : Lean.Name} →
    {args moreInfo : Option String} →
      {role' : Lean.Name} →
        {args' moreInfo' : Option String} →
          { role := role, args := args, moreInfo := moreInfo } =
              { role := role', args := args', moreInfo := moreInfo' } →
            (role = role' → args = args' → moreInfo = moreInfo' → P) → P