(add-pvar-name "P" "Q" (make-arity)) ;;Exercise 20/i ;;Ex 20/ii (define proof (current-proof)) (proof-to-expr-with-formulas proof)