proposition: Lemma size_exp_min_mutual : (forall e1, 1 <= size_exp e1).
proof: Proof. apply_mutual_ind exp_mutind; default_simp. Qed.
imports: Coq.Logic.FunctionalExtensionality Coq.Program.Equality Metalib.Metatheory Metalib.LibLNgen Stlc