proposition: Lemma lc_body_exp_wrt_exp : forall e1 e2, body_exp_wrt_exp e1 -> lc_exp e2 -> lc_exp (open_exp_wrt_exp e1 e2).
proof: Proof. unfold body_exp_wrt_exp; default_simp; let x1 := fresh "x" in pick_fresh x1; specialize_all x1; exp_lc_exists_tac; eauto 7 with lngen. Qed.
imports: Coq.Logic.FunctionalExtensionality Coq.Program.Equality Metalib.Metatheory Metalib.LibLNgen Stlc