 
 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 ty)]
-  ;; [[[[(list #'or-elim A B) or-term] prop] left-proof] right-proof])))
-  [[[[(list #'or-elim% left-type right-type) or-term] prop] left-proof] right-proof])
+  (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]].

      (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))
     [(second t) (nth t 2)]
     (match t
       (['Π [C ✳] (['Π [_ (['Π [_ A] C1] :seq)] (['Π [_ (['Π [_ B] C2] :seq)] C3] :seq)] :seq)] :seq)
       (if (= C C1 C2 C3)
