proposition: Lemma size_typ_min : forall T1, 1 <= size_typ T1.
proof: Proof. pose proof size_typ_min_mutual as H; intuition eauto. Qed.
imports: Coq.Logic.FunctionalExtensionality Coq.Program.Equality Metalib.Metatheory Metalib.LibLNgen Stlc