\vect{x} & = x & x is local \\
\vect{\Lambda\alpha:\kappa.e} & =
\Lambda\alpha:\kappa.\lambda{dPA_{\alpha}}:\patype{\alpha:\kappa}.\vect{e} \\
-\vect{e[\sigma]} & = \vect{e}[\vect{\sigma}] \\
+\vect{e[\sigma]} & = \vect{e}[\vect{\sigma}] \pa{\vect{\sigma}} \\
\vect{e_1 e_2} & = \vect{e_1}\capp\vect{e_2} \\
\vect{\lambda{x}:\sigma.e} & = Clo \vect{\sigma} \vect{\phi} \tau \pa{\tau}
(y_1,\dots,y_n) \\