
%format fst     = "\pi_1 "
%format snd     = "\pi_2 "

%format Either x y = x "+ " y
%format Left    = "\iota_L "
%format Right   = "\iota_R "

%format Mu      = "\mu "
%format InF	    = "in "
%format outF	= "out "

%format cata x = "\llparenthesis "  x  "\rrparenthesis "
%format ana x  = "[\!( " x ")\!]"

%format Inl     = "\kappa_L "
%format Inr     = "\kappa_R "


%format undefined = "\bot "
%format bot = "\bot "


%format °   = "\bullet "
%format ./\.    = "\sqcap "
%format .\/.    = "\sqcup "


%format <*>   = "\times "
%format :*:   = "\times "
%format /\    = "\times "
%format prod p q = "\langle" p "," q "\rangle"


%format <|> = "+ "
%format :+: = "+ "
%format \/  = "+ "
%format coprod p q = "[" p "," q "]"


%format eval x = "\llbracket " x "\rrbracket "


%format Bool      = "\BB "
%format True      = "\true "
%format False     = "\false "
%format not      = "\neg "
%format ||       = "\vee "
%format &&       = "\wedge "
%format ==       = "\equiv "


%format elem = "(\in) "
%format `elem` = "\in "
%format `isSubsetOf` = "\subseteq "
%format `intersection` = "\cap "
%format length x = "|" x "|"

%format empty = "\emptyset "
%format `union` = "\cup "
%format `intersection` = "\cap "
%format singleton x = "\{ " x "\} "
%format delete a x  = x "\setminus \{" a "\}"
%format insert a x  = x "\cup \{" a "\}"


%format return = "\eta "

%format Maybe a = a "_\nabla "
%format Just = "\eta "
%format Nothing = "\nabla "

%format Integer = "\NN"
%format Int = "\NN "


%format delta   = "\delta "
%format phi     = "\phi "
%format rho     = "\rho "
%format lambda  = "\lambda "
%format alpha  = "\alpha "
%format beta  = "\beta "
%format sigma  = "\sigma "

%format delta'
%format phi'
%format rho'
%format lambda'
%format alpha'
%format beta'
%format sigma'




%format LangF x = "{\mathsf{L}}_ " x
%format Lang x = "{\Lang}_ " x
%format denotP x = "\llbracket" x "\rrbracket_P"
%format denotAt ev x = "\llbracket" x "\rrbracket_{ev}"
%format denotL ev x = "\llbracket" x "\rrbracket_\Lang\; " ev 
%format denot x = "\llbracket" x "\rrbracket"


%format Subs    = "\Sigma "
%format Prop    = "P "
%format Event   = "E "

%format Mode    = "\mode "
%format Obl     = "\obl "
%format For     = "\for "
%format swapMode m  = m "^\dagger "


%format satAt ev x = "\llbracket" x "\rrbracket^{\mathcal{A}}_{" ev "}"
%format sat ev x = "\llbracket" x "\rrbracket_{" ev "}"

%format RLLang a = "\mathcal{RL}_{ " a "}"
%format Cst     = "\mathcal{CST} "

%format ATM a   = a
%format CNJ     = "(\wedge) "
%format `CNJ`   = "\wedge "
%format DSJ     = "(\vee) "
%format `DSJ`   = "\vee "
%format IMP     = "(\imp) "
%format `IMP`     = "\imp "
%format NEG   = "\neg "
%format FRA a  = "\forall " a ". "
%format EXA a  = "\exists " a ". "
%format FRT t  = "\forall " t ". "
%format EXT t  = "\exists " t ". "
%format FOR a  x = "\forall " a "\in " x ". "
%format EXS a  x = "\exists " a "\in " x ". "
%format Count n t = "\vert " t "\vert \geq " n ". "

%format prj t a     = t "[ " a "] "

%format Atom a   = "\mathcal{A}_{" a "}"
%format AAEq     = "(=) "
%format `AAEq`   = "= "
%format PPEq     = "(=) "
%format `PPEq`   = "= "
%format PCEq     = "(=) "
%format `PCEq`   = "= "
%format ACEq     = "(=) "
%format `ACEq`   = "= "
%format Rng     = "(\in) "
%format `Rng`   = "\in "


%format freeVars' x = "FV^\mathcal{A}(" x ")"
%format freeVars x = "FV(" x ")"
%format joinVars = "(\uplus) "
%format `joinVars` = "\uplus "

%format neq = "(\neq) "
%format `neq` = "\neq "

%format tup     = "\sigma^1 "
%format tup1
%format tup2
%format att     = "\sigma^2 "
%format sch     = "\Sigma "
%format sch1
%format sch2
%format set     = "R "
%format rel     = "r "
%format db      = "db "
%format db'
%format db1
%format db2


%format t   = "t "
%format t'
%format t0
%format t1
%format t2
%format t3
%format t4


%format f   = "f "
%format f1
%format f1'

%format g   = "g "
%format g1
%format g1'


%format enum   = 
