GitLab

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