
% -- Types of Alternatives ------------------------------------------------------------------------
\begin{figure}
\boxfig{
\begin{center}
\fbox{ $\tyJudge {\Gamma} {\Sigma} {p \to t} {\tau \to \tau'} {\sigma}$ } 
\end{center}
\vspace{-1em}
\[	\ruleIL	{TyAlt}
		{ \begin{array}{rr}
			\theta = [\varphi / r \ \ov{\varphi' / a}]
		  \\
			K :: \forall (r : \%) (\ov{a : \kappa}). 
				\ov{\tau} \to T \ r \ \ov{a} \in \trm{ctorTypes}(T)
		  \quad
			\tyJudge
				{\Gamma, \ \ov{x : \theta(\tau)}}
				{\Sigma}
				{t}
				{\tau'}
				{\sigma}
		  \end{array}
		}
		{ \tyJudgeGS
			{ K \ \ov{x} \to t}
			{ T \ \varphi \ \ov{\varphi'} \to \tau'}
			{ \sigma }
		}
\]

} % boxfig
\smallskip
\caption{Types of Alternatives}
\label{fig:types-of-alternatives}
\end{figure}
