reverse/reverseの証明に戻ってここからです (if (atom x) 't (equal (if (atom (reverse2 x '())) (reverse2 x '()) (reverse2 (reverse2 x '()) '())) x)) (atom x)でなければ(if (atom (reverse2 x '()))が成り立つことはない、が証明されたので ((E 1 Q)…