sig T. kind ty type. kind tm type. type nat ty. type arr (ty -> ty) -> ty. type zero tm. type suc tm -> tm. type lam string -> ty -> tm -> tm. type ap tm -> tm -> tm.