

% -----------------------------------------------------------------------------
\begin{definition}[Substitution]
We use standard capture avoiding substitution over terms, types, kinds, superkinds and type environments. The expression $A[B/x]$ means ``A with B substituted for x". We work up to renaming of bound variables.
\end{definition}


% -----------------------------------------------------------------------------
\begin{definition}[No Fabricated Region Witnesses]

The predicate nofab() is short for ``No fabricated region witnesses'' and refers to the syntactic restriction that the witness constructors $MkMutable$ and $MkConst$ may only appear in the witness list associated with a $\kletregion$. The predicate is defined for value, type, kind and superkind expressions, as all can contain type applications.

\pagebreak{}
Example inference rules are as follows:

$$
	\infer
	{ \rnofab(t~ \varphi)}
	{ \rnofab(t) \quad \rnofab(\varphi)}
$$
$$
	\infer
	{ \rnofab(\varphi_1~ \varphi_2)}
	{ \rnofab(\varphi_1) \quad \rnofab(\varphi_2)}
$$
$$
	\infer
	{ \rnofab(\kletregion~ r~ \kwith~ \ov{w = \delta}~ \kin~ t) }
	{ \rnofab(t) }
$$

Besides this last judgement which ignores the witness list associated with a $\kletregion$, all others are generated by mechanical recursive decent of the syntax tree. Clearly, \\ $\rnofab(MkMutable)$ and $\rnofab(MkConst)$ must be \emph{false}.
\end{definition}