(atom x)でなければ(if (atom (reverse2 x '()))が成り立つことはない、を証明します (J-Bob/prove (defun.reverse) '(((dethm atom/reverse2 (x res) (if (atom x) 't (equal (atom (reverse2 x res)) 'nil))) (reverse2 x res) ; ← ここ！これ！きっと！ …