diff --git a/paper-new/defs.tex b/paper-new/defs.tex
index 11cabf1cc4225d978e2b04c7d96eee2de55fe5aa..e4df2f22d7ce39935a26f9047bc0586f08d1a402 100644
--- a/paper-new/defs.tex
+++ b/paper-new/defs.tex
@@ -40,7 +40,7 @@
 \newcommand{\dnc}[2]{\text{dn}\,{#1}\,{#2}}
 
 
-\newcommand{\ret}{\mathsf{ret}}
+% \newcommand{\ret}{\mathsf{ret}}
 \newcommand{\err}{\mho}
 \newcommand{\zro}{\textsf{zro}}
 \newcommand{\suc}{\textsf{suc}}
@@ -50,7 +50,7 @@
 \newcommand{\casenat}[4]{\text{Case}_\text{nat} ({#1}) \{ \text{no} \to {#2} \alt \text{nat}({#3}) \to {#4} \}}
 \newcommand{\casearr}[4]{\text{Case}_\ra ({#1}) \{ \text{no} \to {#2} \alt \text{fun}({#3}) \to {#4} \}}
 \newcommand{\casedyn}[5]{\text{Case}_\Dyn ({#1}) \{ \text{nat}({#2}) \to {#3} \alt \text{fun}({#4}) \to {#5} \}}
-\newcommand{\bind}[3]{\text{var } {#1} = {#2} \text{ in } {#3}}
+%\newcommand{\bind}[3]{\text{var } {#1} = {#2} \text{ in } {#3}}
 \newcommand{\matchnat}[4]{\text{match } {#1} \text{ with } \{ \textsf {zero} \Rightarrow {#2} \alt \textsf{ suc } {#3} \Rightarrow {#4} \}}
 
 \newcommand{\refl}{\text{refl}}
@@ -174,6 +174,11 @@
 \newcommand{\ptbv}{\text{ptb}^\mathcal{V}}
 \newcommand{\ptbe}{\text{ptb}^\mathcal{E}}
 
+\newcommand{\Ppure}{P}
+\newcommand{\Pk}{P^K}
+\newcommand{\ptbk}{\text{ptb}^K}
+
+
 \newcommand{\upf}{\text{up}}
 \newcommand{\dnf}{\text{dn}
 }
@@ -218,3 +223,9 @@
 
 
 \newcommand{\da}{\downarrow}
+
+\newcommand{\ret}{\text{ret}}
+\newcommand{\bind}[3]{{#1} <- {#2}\, ; \, {#3}}
+
+\newcommand{\piv}{\Pi^\mathcal{V}}
+\newcommand{\pie}{\Pi^\mathcal{E}}
\ No newline at end of file