FastSubst fixes

- lots of fixes
- plus some proofs.
Fixing some import names.