433       \end{center}

   433       \end{center}

   434        

   434        

   435       Many of such rule are called intro-rules and end with 

   435       Many of such rule are called intro-rules and end with 

   436       an ``$I$'', or in case of inductive predicates $\_.intros$.

   436       an ``$I$'', or in case of inductive predicates $\_.intros$.

   437       

   437       

   441 \end{itemize}

   439 \end{itemize}

   442  

   440  

   443 

   441 

   444 \end{document}  

   442 \end{document}