             :by (or-intro-right A <d1>)))
     (have <e> _ :by (or-elim H1 (or A (or B C))
                              <c> <d>)))
-
-  )
-  ;;(qed <e>))
+  (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 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])

(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))))
      (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>)))
