Some progress, some beta stuff

@knuton, would prefer if you merged this in as-is, because otherwise I will have to do lots of nasty rebasing, which I can't be bothered to.

Also, this contains a bunch of lemmas about `bred` / `bstar` you might find useful.