           (have <a> (==> (==> A C) (==> B C) C) :by (H1 C))
           (have <b> (==> (==> B C) C) :by ((<a>) H2))
           (have <c> C :by ((<b>) H3))
-          (showdef <c>)
           (qed <c>)))

       :script
       (assume [x A
                C :type
                z C
                H1 (==> B C)
                H2 (==> A C)]
           (have <a> (==> (==> B C) C) :discharge [H1 z])
           (have <b> (==> (==> A C)
                          (==> B C)
                          C) :discharge [H2 <a>])
           (have <c> (or A B) :discharge [C <b>])
           (showdef <c>)
           (qed <c>)))


(defthm or-elim
  "Elimination rule for logical disjunction."

          (==> B C)
          C)))

(defthm or-intro-left
  "Introduction rule for logical disjunction.
This is the introduction by the left operand."
