%format ::= = "\rightarrow\;\;"
%format ||| = "\;\; |"
%format :- = "\vdash "
%format ::- = "\Vdash "
%format :-> = "\mapsto "
%format ~> = "\leadsto "
%format :> = "\triangleright "
%format \\ = "\Lambda"
%format <== = "\subseteq"
%format env = "\Gamma "
%format envl = "\Delta"
%format emptyenv = env
%format emptyenvl = envl
%format ty = "\tau "
%format identc = "C"
%format identx = "x"
%format identv = "v"
%format alpha = "\alpha "
%format forall = "\forall\! "
%format exists = "\exists\! "
%format dot = "."
%format dots = "\ldots"
%format BigLam = "\Lambda\!\! "
%format dta = data
%format beta = "\beta "
%format eta = "\eta "
%format theta = "\theta "
%format ^ = "{}"
%format ^^^ = "\;"
%format ^^^^ = "\hspace{2em}"
%format ^^^^^ = "\hspace{3em}"
%format =*= = "\doteq "
%format coe = "\gamma "
%format coe' = "\hat{\gamma}"
%format unp = "\diamond "
%format notelem = "\not\in "
%format >< = "\cap "
%format ~~ = "\approx "
%format emptyset = "\emptyset "
%format slash = "\backslash "
%format tya = ty "^{" a "}"
%format tyb = ty "^{" b "}"
%format tyc = ty "^{" c "}"
%format tyl = ty "^{" l "}"
%format tyr = ty "^{" r "}"
%format tyi = ty "_{" i "}"
%format ty' = ty"^\prime"
%format ty'' = "\hat{" ty "}"
%format tyai = ty"^{a}_{i}"
%format tybi = ty"^{b}_{i}"
%format ty1 = ty"^1"
%format ty2 = ty"^2"
%format e' = "\hat{e}"
%format f' = "\hat{f}"
%format a' = "\hat{a}"
%format p' = "\hat{p}"
%format d' = "\hat{d}"
%format sc = "\imath"
%format sc1 = sc "^1"
%format sc2 = sc "^2"
%format sc3 = sc "^3"
%format coe1 = coe "^" 1
%format coe2 = coe "^" 2
%format coen = coe "^" n
%format coeIn = coe
%format coeOut = coe
%format congrab = (coe1 ^^^ . "\ldots" . ^^^ coen)
%format transcoe = (\coe1 coe2 dot coe1 . coe2)
%format spine = "\Phi"
%format Ci = C "_{" i "}"
%format Cdecon = C "^{" unp "}"

%format env__l = env "^" l
%format env__r = env "^" r

%format alpha__l = alpha "^{" l "}"
%format alpha__r = alpha "^{" r "}"
%format alpha_i  = alpha "_{" i "}"

%format (overline(x)) = "\overline{" x "}"
%format manyalpha = "\overline{" alpha "}"
%format manybeta = "\overline{" beta "}"
%format manybetai = manybeta "_{" i "}"
%format manyty = "\overline{" ty "}"
%format manyty'' = "\overline{" ty'' "}"
%format manycoe = "\overline{" coe "}"

%format ECON = "\mbox{\tiny(\textsc{E.CON})}"
%format TXTECON = "\mbox{\textsc{E.CON}}"
%format EVAR = "\mbox{\tiny(\textsc{E.VAR})}"
%format EAPPEXPR = "\mbox{\tiny(\textsc{E.APP.EXPR})}"
%format EAPPUNIV = "\mbox{\tiny(\textsc{E.APP.UNIV})}"
%format ELAMABS = "\mbox{\tiny(\textsc{E.LAM.ABS})}"
%format TXTELAMABS = "\mbox{\textsc{E.LAM.ABS}}"
%format EUNIVABS = "\mbox{\tiny(\textsc{E.UNIV.ABS})}"
%format TXTEUNIVABS = "\mbox{\textsc{E.UNIV.ABS}}"
%format ELET = "\mbox{\tiny(\textsc{E.LET})}"
%format TXTELET = "\mbox{\textsc{E.LET}}"
%format ECASE = "\mbox{\tiny(\textsc{E.CASE})}"
%format TXTECASE = "\mbox{\textsc{E.CASE}}"
%format ECOERCE = "\mbox{\tiny(\textsc{E.COERCE})}"
%format TXTECOERCE = "\mbox{\textsc{E.COERCE}}"
%format ECAST = "\mbox{\tiny(\textsc{E.CAST})}"
%format EAPPCOE = "\mbox{\tiny(\textsc{E.APP.COE})}"
%format TXTEAPPCOE = "\mbox{\textsc{E.APP.COE}}"
%format TXTEAPPC = "\mbox{\textsc{E.APP.EQS}}"
%format TXTEAPPEQS = "\mbox{\textsc{E.APP.EQS}}"

%format PCON = "\mbox{\tiny(\textsc{P.CON})}"
%format PVAR = "\mbox{\tiny(\textsc{P.VAR})}"
%format PAPPPAT = "\mbox{\tiny(\textsc{P.APP.PAT})}"
%format PAPPCOE = "\mbox{\tiny(\textsc{P.APP.COE})}"
%format PAPPUNIV = "\mbox{\tiny(\textsc{P.APP.UNIV})}"
%format PAPPEXIST = "\mbox{\tiny(\textsc{P.APP.EXIST})}"
%format TXTPAPPEXIST = "\mbox{\textsc{P.APP.EXIST}}"
%format TXTPAPPEQS = "\mbox{\textsc{P.APP.EQS}}"

%format TCON = "\mbox{\tiny(\textsc{T.CON})}"
%format TVAR = "\mbox{\tiny(\textsc{T.VAR})}"
%format TAPP = "\mbox{\tiny(\textsc{T.APP})}"
%format TFORALL = "\mbox{\tiny(\textsc{T.FORALL})}"
%format TEXISTS = "\mbox{\tiny(\textsc{T.EXISTS})}"
%format TEQS = "\mbox{\tiny(\textsc{T.EQS})}"

%format CCON = "\mbox{\tiny(\textsc{C.CON})}"
%format CVAR = "\mbox{\tiny(\textsc{C.VAR})}"
%format TXTCVAR = "\mbox{\textsc{C.VAR}}"
%format CAPP = "\mbox{\tiny(\textsc{C.APP})}"
%format CSYM = "\mbox{\tiny(\textsc{C.SYM})}"
%format CTRANS = "\mbox{\tiny(\textsc{C.TRANS})}"
%format CLEFT = "\mbox{\tiny(\textsc{C.LEFT})}"
%format CRIGHT = "\mbox{\tiny(\textsc{C.RIGHT})}"
%format CUNIV = "\mbox{\tiny(\textsc{C.UNIV})}"
%format CINST = "\mbox{\tiny(\textsc{C.INST})}"
%format CREFL = "\mbox{\tiny(\textsc{C.REFL})}"

%format DDATA = "\mbox{\tiny(\textsc{D.DATA})}"
%format TOPLEVEL = "\mbox{\tiny(\textsc{TOPLEVEL})}"

%format CASSUME = "\mbox{\tiny(\textsc{ASSUME})}"
%format CPROVE = "\mbox{\tiny(\textsc{PROVE})}"
%format CREDUCTION = "\mbox{\tiny(\textsc{REDUCTION})}"

%format GSCOPING = "\mbox{\tiny(\textsc{SCOPING})}"
%format GUNIFICATION = "\mbox{\tiny(\textsc{UNIFICATION})}"

%format TXTEASSUME = "\mbox{\textsc{E.ASSUME}}"

%format ftv = "\mathtt{ftv}"
%format sym = "\mathtt{sym}"
%format left = "\mathtt{left}"
%format right = "\mathtt{right}"
%format compose = "\!\!" . "\!\! "

%format decompose = "\mathbf{decompose}"
%format lift = "\mathbf{lift}"

%%format (subst t v) = "[" t "\!/\!" v "]"
%format (subst t v) = [ v := t ]
%format (sub (f) (g)) = "{" f "}_{" g "}"
%format (brack (x)) = "\left<" x "\right>"

%format Ass = "\mathcal{A}"
%format Prv = "\mathcal{P}"
%format Red = "\mathcal{R}"

%format Cn = "\zeta"
%format GR = "\chi"

%format |> = " \; | \; "

%format Substitution = "\theta"
%format substitution = "\theta"
%format substi = "\theta"
%format :-> = "\mapsto"
%format Uni = "\mathcal{U}"

%format pl = p "_" l
%format pr = p "_" r
%format xli = x "^" l "_" i
%format xri = x "^" r "_" i
%format xl = x "^" l
%format xr = x "^" r
%format coeii = coe "^" i
%format coeli = coe "^" l "_" i
%format coeri = coe "^" r "_" i
%format coer = coe "^" r
%format coel = coe "^" l
%format coei = coe "_" i
%format coeIn = coe
%format coeOut = coe
%format coefgintint = coe "^{" fgii "}"
%format coefg = coe "^{" fg "}"

%format skc = "\mbox{skolem type constant}"

%format congrsubst = [ "\overline{" v := ty "}" ]
%%format congrsubstl = [ "\overline{" v "^l" := ty "^l" "}" ]
%%format congrsubstr = [ "\overline{" v "^r" := ty "^r" "}" ]