More cosmetic changes

[PHart3]

1. This PR cleans up the Colimit-code by making the line breaks of huge terms in the equational reasoning more understandable. Previously, they were largely arbitrary. It also does a tiny bit of moving around technical lemmas, but the code itself remains the same.
2. I also shortened the Dockerfile by just running Agda on the final file, which depends on all the other files.