Mistake in explanation in "Under false pretenses"

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.