   (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."

    (assume [H2 (or A B)]
      (assume [H3 A]
        (have <a> (or A (or B C))
              :by (or-intro-left H3 (or B C)))
        [:print-type '<a>])
      (assume [H4 B]
        (have <b1> (or B C)
              :by (or-intro-left H4 C))
        (have <b> (or A (or B C))
              :by (or-intro-right A <b1>)))
      (have <c> _
            :by (or-elim H2 (or A (or B C))
                         <a> <b>)))

            [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]
