huge commit in automation:

huge commit in automation:
- tactics:
  - all tactics used by auto (apply, applys and thus rewrite)
    do handle correctly the subst present in the status
- indexing:
  - demodualte_all (and thus solve_rewriting) reimplemented,
    faster and more correct
- auto:
  - applyS used to apply theorems, remaining goals have a
    depth penalty