ひとつめは 公理の形に合わせるためには(equal (natp (wt (car x))) 't)じゃなくて (natp (wt (car x))でないとだめ ってこと これには9章の後半で出てきた、if-trueを使って都合のいい前提を作る作戦が使える