Instead of using $\lceil x \rceil \in \Gamma$ for some concrete $x$ in the definedness axiom, we should use for all evars $x$, we have $\lceil x \rceil \in \Gamma$. This way, we can use the definedness axiom for any variable, which is necessary if we have to make sure that this variable is fresh in some pattern (e.g., for the side condition of the deduction theorem).
