こんな定理を証明します (dethm ctx?/sub (x y) (if (ctx? x) (if (ctx? y) (equal (ctx? (sub x y)) 't) 't) 't)) そういえばこの間 'tってなんだよ'tって、と思いましたがこれはたぶん定理は常に'tでないといけないので入れてあるってことでしょう 定理証…