кароч там строят терм с типом False или _|_, разобрать всё можно, но нахуй нужно, а если нужно, то бери кококо и https://github.com/maximedenes/native-coq/blob/master/theories/Logic/Hurkens.v или подобный хрюкенс.в дрочи до понимания. Но не нужно ваще. Не парься лол.

ппц ты тупой канеш

@gds да это-то я понял, просто нотация пиздец (и объяснения не для тупых)