proposition: Lemma degree_exp_wrt_exp_of_lc_exp_mutual : (forall e1, lc_exp e1 -> degree_exp_wrt_exp 0 e1).
proof: Proof. apply_mutual_ind lc_exp_mutind; intros; let x1 := fresh "x1" in pick_fresh x1; repeat (match goal with | H1 : _, H2 : _ |- _ => specialize H1 with H2 end); default_simp; eauto with lngen. Qed.
imports: Coq.Logic.FunctionalExtensionality Coq.Program.Equality Metalib.Metatheory Metalib.LibLNgen Stlc