       (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)]
+    (let [[status A B] (decompose-iff-type def-env ctx ty)]
       (when (= status :ko)
-        (throw (ex-info "Not an `and`-type." {:special 'latte.prop/iff-sym%
+        (throw (ex-info "Not an `iff`-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]))))
+      [(list #'iff-sym A B) iff-term])))
 
 (defthm iff-trans
   "Transitivity of logical equivalence."

                                           :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-if%
                                                  :term iff-term
                                                  :type ty}))
            [(list #'iff-elim-if A B) iff-term]))))))

    (qed k)))


(defspecial iff-trans%
  "Transitivity of `<=>`, a special version of [[iff-trans]]."
  [def-env ctx iff-term1 iff-term2]
  (let [[status ty1] (ty/type-of-term def-env ctx iff-term1)]
    (when (= status :ko)
      (throw (ex-info "Cannot type term." {:special 'latte.prop/iff-trans%
                                           :term iff-term1
                                           :from ty1})))
    (let [[status ty2] (ty/type-of-term def-env ctx iff-term2)]
      (when (= status :ko)
        (throw (ex-info "Cannot type term." {:special 'latte.prop/iff-trans%
                                             :term iff-term2
                                             :from ty2})))
      (let [[status A B] (decompose-iff-type def-env ctx ty1)]
        (when (= status :ko)
          (throw (ex-info "Not an `iff`-type." {:special 'latte.prop/iff-trans%
                                                :term iff-term1
                                                :type ty1})))
        (let [[status C D] (decompose-iff-type def-env ctx ty2)]
          (when (= status :ko)
            (throw (ex-info "Not an `iff`-type." {:special 'latte.prop/iff-trans%
                                                  :term iff-term2
                                                  :type ty2})))
          (cond
            (norm/beta-eq? def-env ctx B C)
            [[(list #'iff-trans A B D) iff-term1] iff-term2]
            ;; allow a symmetry
            (norm/beta-eq? def-env ctx B D)
            [[(list #'iff-trans A B C) iff-term1] iff-term2]
            :else
            (throw (ex-info "Type in the middle mismatch"
                            {:special 'latte.prop/iff-trans%
                             :left-lhs-type B
                             :right-lhs-type C
                             :right-rhs-type D}))))))))


