Mizar/本体部/型

変数に型を定義する

such that 関数[ 変数 ];

as mode型;