{P : Sort u} →
  {declName declName' : Lean.Name} →
    Lean.Compiler.LCNF.CacheAuxDeclResult.alreadyCached declName =
        Lean.Compiler.LCNF.CacheAuxDeclResult.alreadyCached declName' →
      (declName = declName' → P) → P