proposition: Lemma open_exp_wrt_exp_rec_degree_exp_wrt_exp_mutual : (forall e2 e1 n1, degree_exp_wrt_exp n1 e2 -> open_exp_wrt_exp_rec n1 e1 e2 = e2).
proof: Proof. apply_mutual_ind exp_mutind; default_simp. Qed.
imports: Coq.Logic.FunctionalExtensionality Coq.Program.Equality Metalib.Metatheory Metalib.LibLNgen Stlc