;; 2022-05-13.  ueb03.scm

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

(add-pvar-name "A" "B" "C" (make-arity))

;; Aufgabe 9/a
(set-goal "(((A -> bot) -> bot) -> A) ->
 (bot -> B) ->
 ((A -> B) -> A) -> A")
(assume "StabA" "EfB" "u")
(use ...)

(proof-to-expr-with-formulas)

;; Aufgabe 9/b
(set-goal "(((A -> bot) -> A) -> A) ->
 (bot -> A) ->
 ((A -> bot) -> bot) -> A")
(assume "PeirceAF" "EfA" "u")
(use ...)

(proof-to-expr-with-formulas)