Improve directory structure and dependencies of formal spec

The formal ledger specification has gone through a series of improvements since it was first used as a base for our formal block header specification, e.g. a reorganization of the directory structure, the removal of the local copy of the set theory library in favor of the use of `agda-sets`, etc. We shall replicate these changes in our formal block header specification.