
\begin{figure}
\boxfig{
\begin{center}
\fbox{ $\kiJudgeGS{\Delta}{\kappa}$ } 
\end{center}

\[	\begin{array}{rll}
		\kiJudge
			{\Gamma}
			{\Sigma[~ \un{\rho} ~]}
			{&\hspace{-0.5em} \un{\rho}} 
			{\%} 
		& (\trm{KiHandle})
	\\[1.5ex]
		\kiJudge
			{\Gamma}
			{\Sigma[~ \un{\trm{const}~ \rho} ~]}
			{&\hspace{-0.5em} \un{\trm{const} \ \rho} }
			{ \iConst \ \un{\rho} }
		& (\trm{KiConst})
	\\[1.5ex]
		\kiJudge
			{\Gamma}
			{\Sigma[~ \un{ \trm{mutable} \ \rho} ~]}
			{&\hspace{-0.5em} \un{\trm{mutable} \ \rho} }
			{ \iMutable \ \un{\rho} }
		& (\trm{KiMutable})
	\end{array}
\]
\[
	\infer	[(\trm{KiPure})]
		{ \kiJudge
			{ \Gamma}
			{ \Sigma}
			{ \un{\rpure \ \sigma}}
			{ \iPure \ \sigma}
		}
		{ \Sigma \vdash \sigma~ \trm{\tbf{pure}}}
\]

\smallskip
} % boxfig
\smallskip
\caption{Kinds of Witnesses}
\label{fig:KindsOfWitnesses}
\end{figure}