A more factored/performant interface for Subst

- Also a demo for the AutoProver showing a considerable
  speedup over the old Subst implementation.
- FastSubst is not implemented yet
- RawSubst2 is not implemented yet.
- Ext/ExprUnifySyntactic2 is ported.