proposition: Lemma degree_exp_wrt_exp_of_lc_exp : forall e1, lc_exp e1 -> degree_exp_wrt_exp 0 e1.
proof: Proof. pose proof degree_exp_wrt_exp_of_lc_exp_mutual as H; intuition eauto. Qed.
imports: Coq.Logic.FunctionalExtensionality Coq.Program.Equality Metalib.Metatheory Metalib.LibLNgen Stlc