(add-pvar-name "A" "B" (make-arity))
(add-pvar-name "P" (make-arity (py "alpha")))
(add-var-name "x" (py "alpha"))
;;Classical existence is written 'excl'
(pp (pf "excl x P x"))
(set-goal "excl x P x")
;; like on paper, it's only an abbreviation
(assume "Hyp")
;; forward reasoning:
;; so far we only had to do backward reasing. we can do forward reasing with 'assert' and 'cut'
(set-goal "A")
(assert "B")
;; two new goals:
;; ?_2:B -> A
;; ?_3:B
;; and cut (goals in other order)
(set-goal "A")
(cut "B")
;;(can also '(get n)' to change goal to ?_n)
;; Exercise 16
;; ...
(define proof (current-proof))
(proof-to-expr-with-formulas proof)
;; can normalize
(define nproof (np proof))
(proof-to-expr-with-formulas nproof)