Здравей, Александър,
Абсолютно си прав, за да има смисъл задачата, би трябвало A да е (поне) едноаргументен предикат. Когато доказвахме формулата на пияниците използвахме едноместен предикат d(x), тук се има предвид същото нещо. Задачата е записана "като за дъска", където A е метапроменлива за произволна формула, която може да съдържа свободни променливи, като е ясно, че същественият случай е този, в който x се среща свободно в A. За да се формализира това в Coq е необходимо тази зависимост да е експлицитно изразена, вместо имплицитно.
Ако направиш x да е nat не би трябвало да използваш нито една аксиома на естествените числа, освен това че множеството е непразно.
За да е доказателството в произволна общност, можеш да приемеш, че имаш домейн Variable D : Set и тогава Variable A : D -> Prop. Тогава обаче в Coq ти трябва допълнително допускане: inhabited T (прочети раздела "Being inhabited" в тази страница).
Можеш да си дефинираш собствен предикат:
Inductive inhabited (A:Type) : Prop := inhabits : A -> inhabited A.
и да добавиш допускането inhabited D към теоремата за пияниците. Тогава доказателството пак би трябвало да работи.
Но да се докаже за естествените числа би трябвало да е достатъчно.