       (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>)))
-      [:print-type '<b>]
       (have <c> _
             :by (or-elim H2 (or A (or B C))
                          <a> <b>)))

   (if (clojure.core/and (seq? t) 
                         (= (count t) 3)
                         (= (first t) #'latte.prop/or))
     [:ok (second t) (nth t 2)]
     (match t
       (['Π [C ✳] (['Π [_ (['Π [_ A] C1] :seq)] (['Π [_ (['Π [_ B] C2] :seq)] C3] :seq)] :seq)] :seq)
       (if (= C C1 C2 C3)


This is (for now) the easiest rule to use for proof-by-cases."
  [def-env ctx [or-term or-type] [prop prop-type] [left-proof left-type] [right-proof right-type]]
  (let [[A B] (decompose-or-type def-env ctx or-type)]
    [[[[(list #'or-elim% A B) or-term] prop] left-proof] right-proof]))

(defthm or-not-elim-left
  "An elimination rule for disjunction, simpler than [[or-elim]].
