⁹More precisely, there is no basic way to prove a contradiction, i.e. 0 has no constructors. If our type theory were inconsistent, then there would be some more complicated way to construct an element of 0.