You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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).
The text was updated successfully, but these errors were encountered:
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).
The text was updated successfully, but these errors were encountered: