     (qed <e>)))
 
 (defthm or-sym
-  "Symmetry of disjunction.
-
-Remark: the proof for this theorem illustrates the non-trivial
-characteristic of or-elimination."
+  "Symmetry of disjunction."
   [[A :type] [B :type]]
   (==> (or A B)
        (or B A)))

(proof iff-elim-if
    :script
  (assume [H (<=> A B)]
    (have a (==> (<=> A B)
                 (==> A B))
          :by (and-elim-left (==> A B) (==> B A)))
    (have b (==> A B) :by (a H))
    (qed b)))

(defthm iff-elim-only-if
  "Elimination rule for logical equivalence.

                 (<=> B A)) :by (iff-intro B A))
    (have d (<=> B A) :by (c a b))
    (qed d)))

(defspecial iff-sym%
  "Symmetry of `<=>`, a special version of [[iff-sym]]."
  [def-env ctx iff-term]
  (let [[status ty] (ty/type-of-term def-env ctx iff-term)]
    (when (= status :ko)
      (throw (ex-info "Cannot type term." {:special 'latte.prop/iff-sym%
                                           :term iff-term
                                           :from ty})))
    (let [[status C _] (decompose-and-type def-env ctx ty)]
      (when (= status :ko)
        (throw (ex-info "Not an `and`-type." {:special 'latte.prop/iff-sym%
                                              :term iff-term
                                              :type ty})))
      (when-not (stx/prod? C)
        (throw (ex-info "Not a product type." {:special 'latte.prop/iff-sym%
                                               :term C})))
      (let [[_ [A _] B] C]
        [(list #'iff-sym A B) iff-term]))))

(defthm iff-trans
  "Transitivity of logical equivalence."
