定理証明手習い (90) J-Bob/define

J-Bob/defineを定義していきます
rewrite/proveは再利用
その後も、'tを返すか定義のリストに証明された定義を付け足すかくらいなので
それほど大きな違いはありません

(rewrite/define defs def seed steps)

証明が成功したら定義のリストに証明された定義を付け足す

(rewrite/define+1 defs1 defs2 pfs)

defs1が古い定義リスト、defs2が新しい定義リスト、pfsは証明のリスト
同じなら証明が失敗したということなので終了
証明のリストの末尾までたどり着いても（めでたく）終了
そうでなければ次の証明

(rewrite/define+ defs pfs)

複数の証明を開始する
ほとんどdefine+1と同じ

(J-Bob/prove defs pfs) pfsを証明する

引数チェックをしてrewrite/define+を呼び出すだけ

J-Bob/defineができたのでpreludeももとにもどして、と
全証明、動きました！