Add detailed documentation using Scribble

[atgeller]

We want to add documentation for every metafunction, describing the purpose and usage, as well as thorough documentation for the reduction relation, typing judgments, and typechecker. The former should make it easier to understand the latter, and the latter hopefully will provide a useful introduction to the WebAssembly language model, as well as being useful reference for working with the Redex model.

This would be nice to get to, but is not a high priority at the moment. I think the current level of comments + the README is sufficient to give a basic understanding of what's going on. However, providing thorough documentation should make the model more accessible and will be useful in the future.

Unfortunately, there aren't Redex hooks for Scribble, so we'll have to defthing everywhere.