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

      (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."

                                           :term iff-term
                                           :from ty}))
      (do
        (let [[status A B] (decompose-iff-type def-env ctx ty)]
          (if (= status :ko)
            (throw (ex-info "Not an `iff`-type." {:special 'latte.prop/iff-elim-if%
                                                  :term iff-term
                                                  :type ty}))
            [(list #'iff-elim-if A B) iff-term]))))))
