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