introduction to coq continued, now i have learned what the codebase is supposed to do when it’s finished