Ссылка на тот факт, что (0 = 1) означает ложь, требует вселенной в MLTT

Это довольно известный факт, что для получения противоречия из неравенства (например, ) в теории типов Мартина-Лоэфа требуется вселенная.$(0=1) \to \bot$

Доказательство также довольно простое - в отсутствие юниверсов мы можем стереть зависимости из любого зависимого типа, чтобы получить простой тип в качестве формы, и, таким образом, доказав, что мы можем доказать для произвольного атома , что, конечно, невозможно.$(0=1) \to \bot$$p \to \bot$$p$

Однако я не могу найти, кто это доказал первым! У кого-нибудь есть ссылка?

Я знаю:

Ян М. Смит, Независимость четвертой аксиомы Пеано от теории типов Мартина-Лёфа без вселенных, Журнал символической логики 53 (3), с. 840-845, 1988.