                                            :term iff-term
                                            :from ty}))
       (do
-        (let [[status A B] (decompose-and-type def-env ctx ty)]
+        (let [[status A B] (decompose-iff-type def-env ctx ty)]
           (if (= status :ko)
-            (throw (ex-info "Not an `and`-type." {:special 'latte.prop/iff-elim-if%
+            (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]))))))

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