proposition: Lemma lc_abs_exists : forall x1 e1, lc_exp (open_exp_wrt_exp e1 (var_f x1)) -> lc_exp (abs e1).
proof: Proof. intros; exp_lc_exists_tac; eauto 6 with lngen. Qed.
imports: Coq.Logic.FunctionalExtensionality Coq.Program.Equality Metalib.Metatheory Metalib.LibLNgen Stlc