MPCTT Textbook Project Modeling and Proving in Computational Type Theory Using the Rocq Prover Gert Smolka pdf Rocq