Проблема разрешимости формул в ИП с одноместными предикатами

[Sonic86]

Не могу понять доказательство разрешимости класса формул в исчислении предикатов с одноместными предикатами у Игошина в книге Математическая логика и теория алгоритмов, в его книге - это теорема 23.2. Утверждение теоремы следующее:

Теорема 23.2. Если формула логики предикатов, содержащая только одноместные предикатные переменные, выполнима, то она выполнима на конечном множестве, содержащем не более $2^n$ элементов, где $n$ — число различных предикатных переменных, входящих в рассматриваемую формулу.

Если лень открывать книгу, то можно прочитать доказательство дословно здесь.

Прежде всего я не могу понять, где автор использует одноместность предикатов (Ctrl-F подтверждает). Уже 3 раза прочел, все равно не понимаю. Попробовал конкретные формулы рассматривать - тоже в голову ничего не приходит.
Вообще, попробую доказательство укоротить и выложить здесь и перечитать, может пойму тогда.
Если эта теорема есть в другом источнике - сообщите пожалуйста.

upd: у меня появилась мысль, что доказывается разрешимость не для всего класса формул с одноместными предикатами, а для более узкого класса: для всех формул ИП с одноместными предикатами, такими, что каждый предикат имеет свою переменную, входящую только в него и не входящую ни в какие другие предикаты (т.е. биекция между предикатами и переменными). Если так, тогда действительно очевидно: просто перебираем для каждого предиката значения $0;1$ - они будут независимы от истинностных значений других предикатов и все...

upd2:

Sonic86 в сообщении #700923 писал(а):

upd: у меня появилась мысль, что доказывается разрешимость не для всего класса формул с одноместными предикатами, а для более узкого класса: для всех формул ИП с одноместными предикатами, такими, что каждый предикат имеет свою переменную, входящую только в него и не входящую ни в какие другие предикаты (т.е. биекция между предикатами и переменными).

Попробовал - получается, что это роли не играет. На самом деле между множеством одноместных предикатов и множеством переменных есть сюрьекция. При проведении индукции просто тогда надо делать подстановку предмета $a$ не в один предикат, а в несколько. А дальше все равно все обеспечивает квантор $K_1x_1$.
А одноместность, видимо, нужна для того, чтобы при подстановке хотя бы одной переменной в предикат из последнего получалось высказывание. Хотя не очевидно.