Erase function lemma (#1053)

* Fix typed erasure calls to _not_ trim inductive masks

* Comment WIP app_construct proof

* Comment WIP erase_function proof

* Prove that functions are preserved by compilation

* Show that inhabitants of product types evaluate to functions through the erasure pipeline

Author: mattam82