ага, i was about to say, что я видать заблуждаюсь в возможности f x = f x. Из чего-то оно должно выплывать.

ок, ⊥ → ⊥ населён, ибо есть id. Да, это означает, что не-абсурд - это истина.