proposition: Lemma nom_to_exp_lc : forall ne, lc_exp (nom_to_exp ne).
proof: Proof. induction ne; simpl; auto. eapply lc_abs_exists with (x1 := x). rewrite open_exp_wrt_exp_close_exp_wrt_exp. auto. Qed.
imports: Metalib.Metatheory Stlc.Definitions Stlc.Lemmas