proposition: Lemma lc_exp_unique : forall e1 (proof2 proof3 : lc_exp e1), proof2 = proof3.
proof: Proof. pose proof lc_exp_unique_mutual as H; intuition eauto. Qed.
imports: Coq.Logic.FunctionalExtensionality Coq.Program.Equality Metalib.Metatheory Metalib.LibLNgen Stlc