(add-pvar-name "A" "B" "C" (make-arity))
(add-pvar-name "P" "Q" (make-arity (py "alpha")))
(add-var-name "x" "y" (py "alpha"))
;;Existence is written exd
;; existence has an intro
(set-goal "all x(P x -> exd x P x)")
(assume "x" "Px")
;; and it needs a term, suppled py pt (parse term)
(intro 0 (pt "x"))
(use "Px")
;;and an elim
(set-goal "exd x P x -> all x(P x -> A) -> A")
(assume "ExHyp" "AllHyp")
;; we can
;;(elim "ExHyp")
;; or use (by-assume ...) which takes an an existence assumption a new var-name and a name for the
;; resulting assumption
(by-assume "ExHyp" "x" "Hyp")
;; note that
;; (use "AllHyp")
;; doesnt work here. It doesnt know which x
(use "AllHyp" (pt "x"))
(use "Hyp")
;;Ex6/i
(set-goal "exd x(P x -> B) -> all x P x -> B")
;; ...
;;Ex6/ii
;; ->
;; ...
;; <-
;...
;;Ex6/iii
;; ...
;;Ex9
(set-goal "(((A -> bot) -> bot) -> A) -> bot -> A")
;; ...
(proof-to-expr-with-formulas (current-proof))
;; note that we also have a function to normalize proof, namely (np 'proof')