Move stuff into Coq chapter
Refactor sections