MPCTT Textbook Project Modeling and Proving in Computational Type Theory Using the Coq Proof Assistant Gert Smolka pdf Coq