А есть примеры, где бы это приводило к проблемам?
В математике, наверное, нет (ожидаемые свойства, видимо, верны, хотя доказать их мучительно трудно, а кое-что и вовсе не доказано). А при написании пруфчекеров это одна из главных проблем. У продвинутых программистов были практические проблемы. Есть такое pi-calculus, или исчисление процессов. Там простенькие программы, вычисляясь параллельно, обмениваются сообщениями. Его используют для для изучения параллельных вычислений (блокировки всякие, как сделать, чтобы два процесса не заблокировали друг друга), а также проверки протоколов (кто-то с кем-то обменивается паролями и секретными ключами, посередине влезает хакер и пытается обмануть, выдавая себя за другого -- получится или нет? есть некоторая теория и практические способы проверки, в том числе специальные программы). В этом исчислении несколько операций, связывающих переменные (как кванторы и лямбды), причём операции непривычные. И там просто не могли понять, как переименовывать связанные переменные, что можно, чего нельзя. В конце концов как-то сделали, видимо, правильно, но никто, конечно, этого не доказал (а если сделали неправильно, хакеры взломают все наши протоколы!)
