Generalize Mapable instances
Rework the expression parser

Now uses a simple version of type inference and can parse every SMTLib expression