fixes the level of equality type
induction principle for equality type added
equality type parameterized over x
separated out the theorems on nat
separated out the theorems on equality
added top level modules for core types and theorems