typing: remove useless notation

typing/records.tex

@@ -164,9 +164,6 @@ atoms defined as:
 where for a record type atom $T$, $\dom_t(T)$ is defined as the set
 of all elements of \ty{string} whose image by $T$ is different from $t$.
 
-We allow us to write $x \orthsum_z y$ as a shorthand for ``$x \orthsum_z y$ is
-well-defined''.
-
 In this case, the litteral expression
 
 \begin{lstlisting}