proposition: Lemma lc_exp_unique_mutual : (forall e1 (proof2 proof3 : lc_exp e1), proof2 = proof3).
proof: Proof. apply_mutual_ind lc_exp_mutind; intros; let proof1 := fresh "proof1" in rename_last_into proof1; dependent destruction proof1; f_equal; default_simp; auto using @functional_extensionality_dep with lngen. Qed.
imports: Coq.Logic.FunctionalExtensionality Coq.Program.Equality Metalib.Metatheory Metalib.LibLNgen Stlc