Mistake in explanation in "Under false pretenses"

[mb64]

The "Under false pretenses" page concludes with a discussion of the "eta for $0$" rule in dependent type theory, saying

we would first need to decide whether the type of any variable in scope is or can be converted to $0$, which is not in general decidable.

This is not true -- definitional equality is (hopefully) decidable, and there are only finitely many variables in scope!

The issue is instead that the same reasoning holds not just for a variable x that's in scope, but for any term M that can be built using the variables in scope. So $\mathsf{true} \equiv \mathsf{false}$ iff the context is inconsistent (i.e. $\Gamma \vdash M : 0$ for a term $M$), which is not decidable.