generic code to ext-lib & refactoring.

- Use coq-ext-lib for basic tactic automation.
- Abstract the canceler with respect to an ordering.
- Separate the unifier from the canceler and introduce
  syntactic vs semantics unification.
- Updating installation instructions.