     (have a _ :by (H1 D))
     (have b D :by (a H3 H2))
     (qed b)))
+
+(defspecial or-sym%
+  "Symmetry of disjunction, a special version of [[or-sym]]."
+  [def-env ctx or-term]
+  (let [[status ty] (ty/type-of-term def-env ctx or-term)]
+    (if (= status :ko)
+      (throw (ex-info "Cannot type term." {:special 'latte.prop/or-sym%
+                                           :term or-term
+                                           :from ty}))
+      (do
+        (let [[status A B] (decompose-or-type def-env ctx ty)]
+          (if (= status :ko)
+            (throw (ex-info "Not an `or`-type." {:special 'latte.prop/or-sym%
+                                                 :term or-term
+                                                 :type ty}))
+            [(list #'or-sym A B) or-term]))))))
 
 (defthm or-not-impl-elim
   "An alternative elimination rule for disjunction."

    (qed <e>)))

(defthm or-sym
  "Symmetry of disjunction.

Remark: the proof for this theorem illustrates the non-trivial
characteristic of or-elimination."
  [[A :type] [B :type]]
  (==> (or A B)
       (or B A)))

          :by (and-elim-right (==> A B) (==> B A)))
    (have b (==> B A) :by (a H))
    (qed b)))

(defspecial iff-elim-only-if%
  "Right (only if) elimination for `<=>`, a special version of [[iff-elim-only-if]]."
  [def-env ctx iff-term]
  (let [[status ty] (ty/type-of-term def-env ctx iff-term)]
    (if (= status :ko)
      (throw (ex-info "Cannot type term." {:special 'latte.prop/iff-elim-only-if%
                                           :term iff-term
                                           :from ty}))
      (do
        (let [[status A B] (decompose-and-type def-env ctx ty)]
          (if (= status :ko)
            (throw (ex-info "Not an `and`-type." {:special 'latte.prop/iff-elim-only-if%
                                                  :term iff-term
                                                  :type ty}))
            [(list #'iff-elim-only-if A B) iff-term]))))))

(defthm iff-sym
  "Symmetry of logical equivalence."
