Assignment for the course Type Theory and Coq, a simple expression compiler with correctness proof in Coq.