定理証明手習い (78) sub-var 〜 sub-e

やっと形式チェックではない処理

(sub-var vars args var) 変数に対応する引数
vars 変数のリスト
args 引数のリスト
var 変数

(sub-es vars args es) （複数の）式の置き換え
(sub-e vars args e) （単独の）式の置き換え

ここも複数の式を置き換える関数を作ってからその特殊系として単独の式の置き換えを作ってる
どうして単独の式の置き換えを使ってからmapするようなやり方をしないんだろうか
できそうな気がするけど

ここでは置き換えた項をさらに再帰的に置き換える、といったことはしてないですね
1ステップ分だけの置き換え
J-Bobはもともとそれしかやってないですしね