;; 2024-11-18.  ueb06.scm

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

(add-var-name "x" (py "alpha"))
(add-predconst-name "P" (make-arity (py "alpha")))

;; 21a
(set-goal
 "exnc x(P x -> all x P x) -> (all x P x -> bot) -> exnc x(P x -> bot)")
(assume "DH" "NegAllH")
;; ...

(proof-to-expr-with-formulas)

;; 21b
(set-goal 
 "exnc x((P x -> bot) -> all x(P x -> bot)) ->
  (((exnc x ((P x -> bot) -> bot)) -> bot) -> bot) ->
  exnc x((P x -> bot) -> bot)")
(assume "DH" "MH")
;; ...

(proof-to-expr-with-formulas)

(proof-to-expr-with-formulas (np (current-proof)))