redex: fix and clean up metafunction expansion

- defer disequation expansion so that generated code
  is linear w/r/t to the number of clauses
- fix variable renaming for disequations