Где гарантии, что какое-то утверждение не мимикрирует под индукцию, как лошади?
Полную гарантию вам даст только страховой полис. Ну либо явное расписывание всего рассуждения из аксиом, что для минимально нетривиальных случаев на практике невозможно.
Но в целом должно быть доказательство перехода, работающее для любого
. И тут возникает общий вопрос - как проверить, что доказательство правильное? Если оно расписано абсолютно формально - то можно чисто синтаксически. Иначе - "чуйкой", что можно довести до полностью формальной записи, а что нельзя.