最初は@を使っていました。
!のdef1 … all #x all #y\,(@ #P #x #y xr #x = #y)

代入を表現する \(@\) があります。

さらに\(@\)を含んで良いものとして #@Form を定義します。
・\({\tt P}\)が#@Form, \({\tt x}\)が#var, \({\tt T}\)が#@Set ⇒ \(@{\tt PxT}\)が#@Form？

・\({\rm fvar}(@{\tt PxT})={\rm fvar}({\tt P})\cup{\rm fvar}({\tt T})\setminus\{\tt x\}\)　if \({\tt w}\)が#var

また\(@\)は同値類の代入として計算されます。