CHANGES:

- improve IMP_REWRITE_TAC
- derived finite dimension from infinite (finitedim.ml)