定理証明手習い (89) J-Bob/prove

(rewrite/prove defs def seed steps)

関数定義なら全域性の主張、
定理なら帰納法の主張を証明します
違うのは種から主張をつくるところだけかな

rewrite/prove+1 (defs pf e)

そこまでの証明が終わっていれば次の証明を行う

rewrite/prove+ (defs pfs)

複数の証明を行う
(list-extend defs (elem1 (car pfs)))というところで
証明済みのものは順次使えるようにしていく

証明は末尾のものから行っていく、というのがここですね

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

引数チェックをしてrewrite/prove+を呼び出すだけ
J-Bob/proveでテストしてたところはあんまりないんですが、
動きそうなとこだけもってきたところうまく動いてるようです