(ld "defpkg.lisp") (certify-book "recursion-by-choose" 1)