Metamathematics in Coq / Roger Dimitri Alexander Hendriks