This is all still pretty ad hoc, but oh well. Also, I have no idea why I had to make those instances in sta_dra global, but it complained about missing instances. Actually, I wonder how they could *not* be global previously...

This strengthens some lemmas that are written using the notion of closednes, shortening some proofs all the way up to barrier.v

This is still a rather horrible proof, though. More work to be done.

this makes it slightlymore annoying to use because we have to elliminate the box. one more reason to have a proof mode ;-)