Summary
- emphasize dedicated rewrite rules for congruences
- moved and exported tactic
- export ML function (towards nonuniform datatypes)
- generalized ML function (towards nonuniform datatypes)
- generalized ML function (towards nonuniform datatypes)
- merge
- renamed confusing variable names