fact: Fixpoint nom_to_exp (ne : n_exp) : exp := match ne with | n_var x => var_f x | n_app e1 e2 => app (nom_to_exp e1) (nom_to_exp e2) | n_abs x e1 => abs (close_exp_wrt_exp x (nom_to_exp e1)) end.
imports: Metalib.Metatheory Stlc.Definitions Stlc.Lemmas