;; 2025-04-17.  solmints.scm

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


(add-predconst-name "A" "B" (make-arity))

;; (a)
;; Es genügt, die Befehle "strip"/"assume" und "use" zu verwenden.
;; Nach Abschluß eines Beweises zeigt (proof-to-expr-with-formulas)
;; den Beweisterm an.
(set-goal "((((A -> B) -> A) -> A) -> B) -> B")

(proof-to-expr-with-formulas)

;; (b)
;; Benutzen sie "prop".
;; Nach Abschluß eines Beweises zeigt (proof-to-expr-with-formulas)
;; den Beweisterm an.
(set-goal "((((A -> B) -> A) -> A) -> B) -> B")

(proof-to-expr-with-formulas)

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