Computer Science Project (INF565 course). Lambda calculus compiler proof in Coq