-\def\av{{\frenchspacing a.v.}}
-
-\def\D{\Delta}
-\def\G{\Gamma}
-\def\ES{\emptyset}
-\def\bigsum{\bigoplus}
-\def\daq{\mathrel{\Downarrow_q}}
-\def\dar{\mathrel{\Downarrow_r}}
-\def\distr{\mathbin\odot}
-\def\dprod{\mathbin\boxtimes}
-\def\dsum{\mathbin\boxplus}
-\def\g{(\G_s, \G_a, \G_g)}
-\def\get#1#2{#1(#2)}
-\def\prod{\mathbin\otimes}
-\def\set#1#2#3{#1[#2 \gets #3]}
-\def\sum{\mathbin\oplus}
-
-\def\Boole{\TT{Boole}}
-\def\Listof{\TT{ListOf}}
-\def\Setof{\TT{SetOf}}
-\def\Str{\TT{String}}
-\def\Num{\TT{Num}}
-
-\def\All{\TT{All}}
-\def\Exp{\TT{Exp}}
-\def\F{\TT{F}}
-\def\For{\TT{For}}
-\def\Fst{\TT{Fst}}
-\def\Fsts{\TT{Fsts}}
-\def\Fun{\TT{Fun}}
-\def\Gen{\TT{Gen}}
-\def\Istrue{\TT{IsTrue}}
-\def\Match{\TT{Match}}
-\def\Name{\TT{Name}}
-\def\Pattern{\TT{Pattern}}
-\def\Property{\TT{Property}}
-\def\Snd{\TT{Snd}}
-\def\Src{\TT{Src}}
-\def\Unquote{\TT{Unq}}
-\def\T{\TT{T}}
-
-\def\GP#1{\TT{<#1>}}
+\newcommand\av{{\frenchspacing a.v.}}
+
+\newcommand\D{\Delta}
+\newcommand\G{\Gamma}
+\newcommand\ES{\emptyset}
+\newcommand\bigsum{\bigoplus}
+\newcommand\daq{\mathrel{\Downarrow_q}}
+\newcommand\dar{\mathrel{\Downarrow_r}}
+\newcommand\distr{\mathbin\odot}
+\newcommand\dprod{\mathbin\boxtimes}
+\newcommand\dsum{\mathbin\boxplus}
+\newcommand\g{(\G_s, \G_e, \G_g)}
+\newcommand\get[2]{#1(#2)}
+\newcommand\sdiff{\mathbin\ominus}
+\newcommand\set[3]{#1[#2 \gets #3]}
+\newcommand\sprod{\mathbin\otimes}
+\newcommand\ssum{\mathbin\oplus}
+
+\newcommand\Boole{\TT{Boole}}
+\newcommand\Listof{\TT{ListOf}}
+\newcommand\Setof{\TT{SetOf}}
+\newcommand\Str{\TT{Str}}
+\newcommand\Num{\TT{Num}}
+
+\newcommand\All{\TT{All}}
+\newcommand\Exp{\TT{Exp}}
+\newcommand\F{\TT{F}}
+\newcommand\For{\TT{For}}
+\newcommand\Fst{\TT{Fst}}
+\newcommand\Fsts{\TT{Fsts}}
+\newcommand\Fun{\TT{Fun}}
+\newcommand\Gen{\TT{Gen}}
+\newcommand\Head{\TT{Head}}
+\newcommand\Istrue{\TT{IsT}}
+\newcommand\Keep{\TT{Keep}}
+\newcommand\Match{\TT{Match}}
+\newcommand\Name{\TT{Name}}
+\newcommand\Pattern{\TT{Pattern}}
+\newcommand\Proj{\TT{Proj}}
+\newcommand\Property{\TT{Property}}
+\newcommand\Snd{\TT{Snd}}
+\newcommand\Src{\TT{Src}}
+\newcommand\Unquote{\TT{Unq}}
+\newcommand\T{\TT{T}}
+
+\newcommand\GP[1]{\TT{<#1>}}
+
+\newcommand\Set{\textsf{Set}}
+\newcommand\Prop{\textsf{Prop}}
+\newcommand\MainConclusion{\textsf{MainConclusion}}
+\newcommand\MainHypothesis{\textsf{MainHypothesis}}
+\newcommand\occurrence{\textsf{occurrence}}
+\newcommand\refObj{\textsf{refObj}}