Simple Theorem Prover

"Programming Language Theory and its Implementation"
を流し読みして、Common Lispで書かれたThorem Proverを
Clojureで書き直し。

http://gist.github.com/823632

・・・なんですが、イマイチ動きません。
以下の例は動いているけど。

(rewrite '(((not (x >= y)) = (x < y))) '(not (1 >= 2))) ;=> (1 < 2)

オリジナルコードでfree variableを使っている
rewrite周辺は、考え直さないといけない。