{P : Sort u} →
  {env : Lean.Kernel.Environment} →
    {name : Lean.Name} →
      {env' : Lean.Kernel.Environment} →
        {name' : Lean.Name} →
          Lean.Kernel.Exception.unknownConstant env name = Lean.Kernel.Exception.unknownConstant env' name' →
            (env = env' → name = name' → P) → P