;; 2022-05-03.  ueb02.scm

;; (load "~/git/minlog/init.scm")

;; Aufgabe 6.

(add-var-name "x" "y" "z" (py "alpha"))
(add-pvar-name "P" (make-arity (py "alpha")))

(set-goal "all x(((P x -> bot) -> bot) -> P x) -> excl x(P x -> all x P x)")
(assume "u" "v")
(use "v" (pt "x")) ;x needed because the system doesn't know which term to take
(assume ...)
...

(proof-to-expr-with-formulas)