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

            :by (or-intro-right A <d1>)))
    (have <e> _ :by (or-elim H1 (or A (or B C))
                             <c> <d>)))

  )
  ;;(qed <e>))

(defthm or-assoc-conv
  [[A :type] [B :type] [C :type]]


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