+\begin{table}
+\caption{\label{tab:wfl2} Well-formedness rules for level 2 patterns.\strut}
+\hrule
+\[
+\renewcommand{\arraystretch}{3.5}
+\begin{array}{@{}c@{}}
+ \inference[\sc Constr]
+ {P_i :: D_i & \forall i,j, i\ne j => \DOMAIN(D_i) \cap \DOMAIN(D_j) = \emptyset}
+ {\BLOB[P_1,\dots,P_n] :: D_i \oplus \cdots \oplus D_j} \\
+ \inference[\sc TermVar]
+ {}
+ {[\mathtt{term}]~x :: x : \mathtt{Term}}
+ \quad
+ \inference[\sc NumVar]
+ {}
+ {\mathtt{number}~x :: x : \mathtt{Number}}
+ \\
+ \inference[\sc IdentVar]
+ {}
+ {\mathtt{ident}~x :: x : \mathtt{String}}
+ \quad
+ \inference[\sc FreshVar]
+ {}
+ {\mathtt{fresh}~x :: x : \mathtt{String}}
+ \\
+ \inference[\sc Success]
+ {}
+ {\mathtt{anonymous} :: \emptyset}
+ \\
+ \inference[\sc Fold]
+ {P_1 :: D_1 & P_2 :: D_2 \oplus (x : \mathtt{Term}) & \DOMAIN(D_2)\ne\emptyset & \DOMAIN(D_1)\cap\DOMAIN(D_2)=\emptyset}
+ {\mathtt{fold}~P_1~\mathtt{rec}~x~P_2 :: D_1 \oplus D_2~\mathtt{List}}
+ \\
+ \inference[\sc Default]
+ {P_1 :: D \oplus D_1 & P_2 :: D & \DOMAIN(D_1) \ne \emptyset & \DOMAIN(D) \cap \DOMAIN(D_1) = \emptyset}
+ {\mathtt{default}~P_1~P_2 :: D \oplus D_1~\mathtt{Option}}
+ \\
+ \inference[\sc If]
+ {P_1 :: \emptyset & P_2 :: D & P_3 :: D }
+ {\mathtt{if}~P_1~\mathtt{then}~P_2~\mathtt{else}~P_3 :: D}
+ \qquad
+ \inference[\sc Fail]
+ {}
+ {\mathtt{fail} : \emptyset}
+%% & | & \verb+if+~\NT{meta}~\verb+then+~\NT{meta}~\verb+else+~\NT{meta} \\
+%% & | & \verb+fail+
+\end{array}
+\]
+\hrule
+\end{table}
+