Redex: parameterized disequations

refactor the pattern unifier and tests to handle
disequations with parameters correctly
Redex: rework metafunction compilation/search for parameters
Redex: corrections for disequations in generator

- handle parameters correctly when simplifying disequations
- rework term generation/disequation checking for parameters
- fix define-extended-metafunction w/r/t the above