証明したい式で
 for x ... を使った場合には
 proof
  let x;
  let x be mode型;
  ...
 
 for x st ～を使った場合には
 proof
  let x be set such that ～
  ...
 証明したい式で
 ex  y ...を使った場合には
 proof
  take y;
  ...
 定義定理などで外部ファイルに ex A と書かれている場合には
 consider a ～ by 外部ファイル名:番号;
 証明したい式で
 x being 型 を使った場合には
  let x be 型;
 
 C言語で表すとすると、beingはポインタ設定、beは値を定義している。
 即ち、
 int *x;
 int a; x=&a
 とすることで、*xに値を代入できるようになるのと同様である。
 変数を使う場合には、$変数名 とする。
 
 defpred P[Nat] means $1
 $1は変数、
 $～。～は英数字とする。
 
 reserve a for set;
 $a
----------------------------------------------------------
 Aを仮定する
  assume A;
 A then B such that
 ...
 thus 証明済み式;
 end;
----------------------------------------------------------
新しい変数を導入する場合には
 set r;
----------------------------------------------------------
いくつかの変数の属性を持った、新しい変数を作る
 cluster