{P : Sort u} →
  {className : Lean.Name} →
    {isNotation : Bool} →
      {findArgs className' : Lean.Name} →
        {isNotation' : Bool} →
          {findArgs' : Lean.Name} →
            { className := className, isNotation := isNotation, findArgs := findArgs } =
                { className := className', isNotation := isNotation', findArgs := findArgs' } →
              (className = className' → isNotation = isNotation' → findArgs = findArgs' → P) → P