proposition: Lemma size_exp_min : forall e1, 1 <= size_exp e1.
proof: Proof. pose proof size_exp_min_mutual as H; intuition eauto. Qed.
imports: Coq.Logic.FunctionalExtensionality Coq.Program.Equality Metalib.Metatheory Metalib.LibLNgen Stlc