namespace TermVar: Term
namespace TypeVar: Type

sort Term
    inh ctx  TermVar
    inh tctx TypeVar
    | TmVar (x@ctx)
    | TmAbs (x: Term) (t: Type) [z: TermVar]
        x.ctx = lhs.ctx, z
    | TmApp (t1: Term) (t2: Term)
    | TmTApp (t1: Term) (t: Type)
    | TmTAbs (t1: Term) [t: TypeVar]
        t1.ctx = lhs.ctx
        t1.tctx = lhs.tctx, t
    | TmTop
    | TmTuple (e1: Term) (e2: Term)
    | TmInt {Int}
    | TmCast (co: Coercion) (e: Term)

sort Type
    inh tyctx TypeVar
    | TyVar (t@tyctx)
    | TyArr (t1: Type) (t2: Type)
    | TyAll (t1: Type) [t: TypeVar]
        t1.tyctx = lhs.tyctx, t
    | TyInt
    | TyTop
    | TyProd (t1: Type) (t2: Type)

sort Coercion
    inh tycoctx TypeVar
    | CoId
    | CoTrans (co1: Coercion) (co2: Coercion)
    | CoTop (ty: Type)
    | CoBot (ty: Type)
    | CoArrow (co1: Coercion) (co2: Coercion)
    | CoTuple (co1: Coercion) (co2: Coercion)
    | CoProj1 (ty2: Type)
    | CoProj2 (ty1: Type)
    | CoAll (co1: Coercion)
    | CoDistArrow
    | CoTopArrow
    | CoTopAll
    | CoDistAll