{P : Sort u} →
  {declName : Lean.Name} →
    {tacticKinds : Array Lean.Name} →
      {declName' : Lean.Name} →
        {tacticKinds' : Array Lean.Name} →
          { declName := declName, tacticKinds := tacticKinds } =
              { declName := declName', tacticKinds := tacticKinds' } →
            (declName = declName' → tacticKinds = tacticKinds' → P) → P