同一視したところを区別し直して
形式的な証明としては完璧なものが作れる場合
あらためて同一視の概念を形式化することに
どんな意味があると思いますか？