             [latte-kernel.syntax :as stx]
             [latte-kernel.typing :as ty]
             [latte-kernel.norm :as norm]
+            [latte-kernel.unparser :as unparser]
             [latte.core
              :as latte
              :refer [defthm defimplicit definition proof assume have qed]

    (==> (==> A C)
         (==> B C)
         C)))

(defthm or-intro-left%
  "Introduction rule for logical disjunction.

  (forall [C :type]
    (==> (==> A B C)
         C)))

(defn and-unparser [term]
  (match
   term
   (['Π [C '✳]
     (['==> (['==> A B C1] :seq)
       C2] :seq)] :seq) (if (= C C1 C2)
                          [(list 'and A B) true]
                          [term false])
   (['Π [C '✳]
     (['==> (['==> A (['==> B C1] :seq)] :seq)
       C2] :seq)] :seq) (if (= C C1 C2)
                          [(list 'and A B) true]
                          [term false])
   :else [term false]))

;; (and-unparser '(Π [X ✳] (==> (==> A B X) X)))
;; (and-unparser '(Π [X ✳] (==> (==> A (==> B X)) X)))

(unparser/register-unparser! :and and-unparser)

(defthm and-intro%
  "Introduction rule for logical conjunction."
