{\bf Inference Rules}
say that ax:AX refers to the previous Axioms list...
-\begin{table}[!h]
-\hrule\vspace{0.1cm}
-\begin{tabular}{p{0.34\textwidth}r}
- $\Gamma, x:A, \Delta \vdash x:A$ & $(Proj)$\\
- $\Gamma \vdash ax : AX$ & $(Const)$\\
- $\frac{\Gamma,x:A \vdash M:Q}{\Gamma \vdash \lambda x:A.M: A \to Q}$ &
- $(\to_i)$\\
- $\frac{\Gamma \vdash M: A \to Q \hspace{0.5cm}\Gamma \vdash N: A}
- {\Gamma \vdash M N: Q}$ & $(\to_e)$\\
- $\frac{\Gamma \vdash M:P}{\Gamma \vdash \lambda x:\N.M: \forall x.P}(*)$ &
- $(\forall_i)$\\
- $\frac{\Gamma \vdash M :\forall x.P}{\Gamma \vdash M t: P[t/x]}$ &
- $(\forall_e)$
-\end{tabular}\vspace{0.1cm}
-\hrule
-\caption{\label{tab:HArules}Inference rules}
-\end{table}{lr}
+%\begin{table}[!h]
+%\hrule\vspace{0.1cm}
+%\begin{tabular}{p{0.34\textwidth}r}
+
+ $$\Gamma, x:A, \Delta \vdash x:A ~~~ (Proj)$$
+ $$ \Gamma \vdash ax : AX~~~ (Const)$$
+ $$\frac{\Gamma,x:A \vdash M:Q}{\Gamma \vdash \lambda x:A.M: A \to Q} ~~~ (\to_i)$$
+ $$\frac{\Gamma \vdash M: A \to Q \hspace{0.5cm}\Gamma \vdash N: A}
+ {\Gamma \vdash M N: Q} ~~~ (\to_e)$$
+ $$\frac{\Gamma \vdash M:P}{\Gamma \vdash \lambda x:\N.M: \forall x.P}(*) ~~~
+ (\forall_i)$$
+ $$\frac{\Gamma \vdash M :\forall x.P}{\Gamma \vdash M t: P[t/x]}
+ ~~~ (\forall_e)$$
+
+%\end{tabular}\vspace{0.1cm}
+%\hrule
+%\caption{\label{tab:HArules}Inference rules}
+%\end{table}{lr}
%\[
% (\land_i)\frac{\Gamma \vdash M:A \hspace{1cm}\Gamma \vdash N:B}