proposition: Lemma size_typ_min_mutual : (forall T1, 1 <= size_typ T1).
proof: Proof. apply_mutual_ind typ_mutind; default_simp. Qed.
imports: Coq.Logic.FunctionalExtensionality Coq.Program.Equality Metalib.Metatheory Metalib.LibLNgen Stlc