HARD: Math unit error checking

[M-Sitaraman]

Proper formulation of inductive definition checking

[yushan87]

@M-Sitaraman If my memory doesn't fail me, the current math type system does not type check the right hand side of any definition. Something wasn't working quite right with it, but it might be very hard to fix it.