この証明がもうちょっと短くできますねと書いてあります (J-Bob/prove (dethm.in-first-of-pair) '(((dethm in-second-of-pair (a) (equal (in-pair? (pair a '?)) 't)) nil ((1 1) (pair a '?)) ((1) (in-pair? (cons a (cons '? '())))) ((1 Q 1) (first-o…