%format . = "."
%%%format ::= = "\rightarrow\;\;"
%format ||| = "\;\; |"
%format mid = "\;\; |"
%format intersect = "\cap"
%format :- = "\vdash "
%format ::- = "\Vdash "
%format ::/- = "\not\Vdash"
%format :-> = "\mapsto "
%format ~> = "\leadsto "
%format :> = "\triangleright "
%format \\ = "\Lambda"
%format <== = "\subseteq"
%format </= = "\not\subseteq"
%format env = "\Gamma"
%format envl = "\Gamma^{" l "}"
%format emptyenv = env
%format emptyenvl = envl
%format ty = "\tau "
%format tya = "\tau^{" a "}"
%format identc = "C"
%format identx = "x"
%format identv = "v"
%format alpha = "\alpha "
%format forall = "\forall\! "
%format exists = "\exists\! "
%format impl = "\sharp\! "
%format implicit = "\mathbf{implicit}"
%format imp = "\mathbf{imp}"
%format dot = "."
%format dots = "\ldots"
%format BigLam = "\Lambda\!\! "
%format dta = data
%format beta = "\beta "
%format eta = "\eta "
%format theta = "\theta "
%format iota = "\iota"
%format tau = "\tau"
%format rho = "\rho"
%format varrho = "\varrho"
%format sigma = "\sigma"
%format ^ = "{}"
%format ^^^ = "\;"
%format ^^^^ = "\hspace{2em}"
%format ^^^^^ = "\hspace{3em}"
%format +++ = "\cup"
%format =*= = "\sim"
%format coe = "\gamma "
%format coe' = "\hat{\gamma}"
%format unp = "\diamond "
%format notelem = "\not\in "
%format `subset` = "\subseteq"
%format `notsubset` = "\not\subseteq"
%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 tyx = ty"^{" x "}"
%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 manyv = "\overline{" v "}"
%format manyv1 = "\overline{" v1 "}"
%format manyvl = "\overline{" vl "}"
%format manyvr = "\overline{" vr "}"
%format manyv' = "\overline{" v' "}"
%format manyx = "\overline{" x "}"
%format star = "\star"

%format ECON = "\mbox{\tiny(\textsc{E.CON})}"
%format TXTECON = "\mbox{\textsc{E.CON}}"
%format EVAR = "\mbox{\tiny(\textsc{E.VAR})}"
%format EAPP = "\mbox{\tiny(\textsc{E.APP})}"
%format EEQ = "\mbox{\tiny(\textsc{E.EQ})}"
%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 ELETX = "\mbox{\tiny(\textsc{E.LET.X})}"
%format ELETP = "\mbox{\tiny(\textsc{E.LET.PAT})}"
%format EIMPLICIT = "\mbox{\tiny(\textsc{E.IMPLICIT})}"
%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 EEQABS = "\mbox{\tiny(\textsc{E.EQ.ABS})}"
%format TXTEEQABS = "\mbox{\textsc{E.EQ.ABS}}"
%format EAPPEQ = "\mbox{\tiny(\textsc{E.APP.EQ})}"
%format TXTEAPPEQ = "\mbox{\textsc{E.APP.EQ}}"
%format EBOTTOM = "\mbox{\tiny(\textsc{E.BOTTOM})}"
%format TXTEBOTTOM = "\mbox{\textsc{E.BOTTOM}}"

%format ENVTY = "\mbox{\tiny(\textsc{E.TY})}"
%format ENVIMPL = "\mbox{\tiny(\textsc{E.IMPL})}"
%format ENVVAR = "\mbox{\tiny(\textsc{E.VAR})}"
%format ENVASSUM = "\mbox{\tiny(\textsc{E.ASSUM})}"
%format ENVOBL = "\mbox{\tiny(\textsc{E.OBL})}"

%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 TARR = "\mbox{\tiny(\textsc{T.ARR})}"
%format TFORALL = "\mbox{\tiny(\textsc{T.FORALL})}"
%format TEXISTS = "\mbox{\tiny(\textsc{T.EXISTS})}"
%format TEQS = "\mbox{\tiny(\textsc{T.EQS})}"
%format TIMPLICIT = "\mbox{\tiny(\textsc{T.IMPLICIT})}"
%format TIMPL = "\mbox{\tiny(\textsc{T.IMPL})}"

%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 CSEQ    = "\mbox{\tiny(\textsc{C.SEQ})}"

%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 iftv = "\mathtt{iftv}"
%format itv = "\mathtt{itv}"
%format otv = "\mathtt{otv}"
%format sym = "\mathtt{sym}"
%format cseq = "\mathtt{seq}"
%format left = "\mathtt{left}"
%format right = "\mathtt{right}"
%format compose = "\circ"

%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 (sub' (f) (g)) = f "_{" g "}"
%format (brack (x)) = "\left<" x "\right>"
%format (sup' (f) (g)) = f "^{" g "}"

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

%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
%firnat coen = coe "_" n
%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" "}" ]

%format hsym = "sym"

%format t1
%format t2
%format ty1
%format ty2
%format ty3
%format ty4
%format coe1
%format coe2
%format coe3
%format coe4
%format v1
%format v2
%format v3
%format e1
%format e2
%format e3
%format x1
%format x2
%format x3
%format x4
%format x5
%format x6
%format a1
%format a2
%format a3
%format p1
%format p2
%format p3
%format env1
%format env2
%format vl = v "^" l
%format vr = v "^" r
%format rho'
%format rho1
%format rho2
%format rho3
%format rho4
%format D1
%format D2
%format s1
%format s2
%format tau1
%format tau2
%format tau3
%format tau4
%format tau5
%format tau6
%format tau7
%format tau8
%format << = "\llbracket"
%format >> = "\rrbracket"
%format (semb (z)) = << z >>
%format `union` = "\cup"
%format coe5
%format coe6
%format Gamma = "\Gamma"
%format Gamma0
%format Gamma1
%format Gamma2
%format Gamma3
%format Gamma4
%format Gamma5
%format Gamma6
%format ... = "\ldots"