次を区別しなくてはならない。
- 命題
- 証明〈証拠〉
- 判断〈主張〉シーケント
- 質問〈問題 | 問い合わせ〉シーケント
- フォワードリーズニング（推論ルール含む）
- バックワードリーズニング（バックワード推論ルール含む）
定理は、証拠〈証明〉を引数として証拠を返す関数で、その型プロファイルがステートメント。判断シーケントは、コンテキストとターゲット命題のペアだが、意味的には証明項の存在の主張〈メタ命題〉。質問シーケント＝ゴールは、コンテキストとターゲット命題のペアではあるが、証明項が不明で未知ラベル〈未知数〉になっている。
次の混乱がある。
- 命題（型）と証拠（要素）の混同
- 命題へのオペレーター（論理コネクティブ | 型演算）と証明へのオペレーター（推論 | 基本リーズニング | ルール）の混同
- 定理と、その定理を使ったルール（ポスト結合リーズニング）の混同
- 推論の意味が、定理または証明の基本構成素（関数）と、リーズニングの基本構成素（高階関数）でオーバーロードされている。どちらも関数だが、命題の要素が引数か、シーケントの集合が引数かの違いがある。
言葉として次が欠けている。
- FR＝フォワードリーズニング
- BR＝バックワードリーズニング
- FRルール＝FRの基本構成素
- BRルール＝BRの基本構成素
- 証明機械と証明状態〈ステージ〉
- FRコマンド（状態遷移）
- BRコマンド＝タクティク（状態遷移）
ステージには判断と質問がいくつかあり、ステージ自体にコンテキスト（ステージ・コンテキスト＝暗黙のコンテキスト）が付いている。コンテキストの変更は重要な操作になる。ステージコンテキストの背後にライブラリコンテキストがある。
ライブラリ、コンテキスト、ステージ、判断、質問、リーズニングルール、リーズニングコンビネータなど、命題以外のメカニズムを理解するのが困難。
追記：まとめ
「混同するな、区別しよう」「同じだから区別するな」を標語にまとめれば：
- 命題とその証拠は違う。
- 証拠〈witness〉と証明〈proof〉は同じ。
- 証拠と要素〈element〉も（宇宙多相で）同じ。
- 証明にプロファイル〈シーケント〉とオプショナルに名前を明示すると定理
- 定理の引数は命題ではなくて証拠。
- 定理の戻り値も命題ではなくて証拠。
- 証明とリーズニングはまったく違う。
- 定理はリーズニングの基本構成素になる。
- リーズニングの基本構成素をルールと呼ぶ。
- 定理と推論規則〈ルール〉と基本リーズニングは同じ。
- 証明／定理は、FRコマンドに埋め込める。
apply 定理 - 証明／定理は、BRコマンドに埋め込める。
deapply 定理だが、タクティク名は apply 、最悪。 - リーズニング（FRとBR)は、リーズニングステージの時間的推移過程を表すリーズニング図〈リーズニンググラフ〉で表現できる。
- リーズニング図のトランジションがリーズニング・コマンドで引き起こされる。
