Split out Substitution.v into separate `sigma` library

[dorchard]

As in the title, we want to separate Substitution.v into its own package (may require some tidy up).

[dorchard]

Plan to do this in January once the rewriting rules are closed.