proposition: Lemma lc_set_exp_of_lc_exp : forall e1, lc_exp e1 -> lc_set_exp e1.
proof: Proof. intros e1; intros; pose proof (lc_set_exp_of_lc_exp_size_mutual (size_exp e1)); intuition eauto. Qed.
imports: Coq.Logic.FunctionalExtensionality Coq.Program.Equality Metalib.Metatheory Metalib.LibLNgen Stlc