対応表：
| 定理記述 | 関数定義 |
| 定理のステートメント | 関数{定義}?のヘッド |
| 証明項 | 計算項 |
| 定理記述する | 関数定義する |
| から導出された定理 | から定義された定理 |
構文と意味は混同される。
- 関数そのもの（型の圏の射）と関数定義という構文対象
- 定理そのもの（命題の圏の射）と定理記述という構文対象
モノと行為が混同される。
- 証明： 定理記述の証明項と証明すること〈導出〉
- 定義： 関数定義のボディと定義すること
別な対応表：
| 関数 | 定理 |
| 関数定義 | 定理記述 |
| 計算〈関数〉 | 証明 |
| 計算項〈関数項?〉 | 証明項 |
| 定義する | 証明する |
| から定義する | 導出する |
| 定義する | リーズニングする |
言い回しの対応：
- 関数〈計算〉 ←→ 証明
- 計算 ←→ 証明
- 定義する ←→ 証明する
- から定義する ←→ から導出する
- 定義する ←→ リーズニングする
「証明 vs リーズニング」の対比はあるが、「関数 vs 定義行為」は言及されない。関数をコマンドを使って定義することがない。強いて言えばコンビネータプログラミング。
