;; Aufgabe 8

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

(set-goal "all x(F -> Q x) -> exd x (Q x -> F) ord all x Q x -> exd x(Q x -> all x Q x)")
(assume "EfQ" "LPO")
;; ...

(set-goal "all x (Q x ord (Q x -> F)) -> exd x(Q x -> all x Q x) -> exd x (Q x -> F) ord all x Q x")
(assume "LEM" "Drinker")
;; ...