{P : Sort u} →
  {name : Lean.Name} →
    {s : Lean.Term} →
      {name' : Lean.Name} →
        {s' : Lean.Term} →
          Lean.PrettyPrinter.Delaborator.AppImplicitArg.optional name s =
              Lean.PrettyPrinter.Delaborator.AppImplicitArg.optional name' s' →
            (name = name' → s = s' → P) → P