           (throw (ex-info "Type in the middle mismatch" {:special 'latte.prop/impl-trans%
                                                          :left-rhs-type B
                                                          :right-lhs-type B'})))
-        [(list #'iff-trans A B C) impl-term1 impl-term2])))))
+        [[(list #'iff-trans A B C) impl-term1] impl-term2])))))
 
 (definition absurd
   "Absurdity."

                                           :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]))))))

    (have b (==> A B) :by (a H))
    (qed b)))

(defn decompose-iff-type
  [def-env ctx t]
  (let [[status L R] (decompose-and-type def-env ctx t)]
    (if (= status :ko)
      [:ko nil nil]
      (let [[status A B] (decompose-impl-type def-env ctx L)]
        (if (= status :ko)
          [:ko nil nil]
          [:ok A B])))))

(defspecial iff-elim-if%
  "Left (if) elimination for `<=>`, a special version of [[iff-elim-if]]."
  [def-env ctx iff-term]
