Implement Ax rule correctly

This updates the expression datatype slightly
Fix a bug in type substitution
Compile quantifiers