Fixing naming problem so that coq_makefile works.

- This is to get around a bug in coq_makefile.
Fixing ExprDemo.
finished proofs in Lambda/ExprLift