Type Prop プロファイル シーケント 型判断プロファイル 命題判断シーケント 型問題プロファイル 命題問題シーケント 計算合成〈synthesis〉 証明合成 計算合成コマンド 証明合成コマンド 順方向計算合成コマンド 順方向証明合成コマンド 逆方向計算合成コマ…

Type Prop 型 命題 計算 証明 関数 定理 定数 前提なし定理 組み込み関数・定数 公理 プロファイル シーケント フルかりー化プロファイル 片側シーケント 既存関数のプロファイル宣言 事実（定理の名前とシーケント） サブルーチン（一例） ルール 型の要素 …