 (proof iff-elim-if
     :script
   (assume [H (<=> A B)]
-    (have a (==> (<=> A B)
+    have (a (==> (<=> A B)
                  (==> A B))
-          :by (and-elim-left (==> A B) (==> B A)))
+           :by (and-elim-left (==> A B) (==> B A)))
     (have b (==> A B) :by (a H))
     (qed b)))
+
+(defspecial iff-elim-if%
+  "Left (if) elimination for `<=>`, a special version of [[iff-elim-if]]."
+  [def-env ctx iff-term]
+  (let [[status ty] (ty/type-of-term def-env ctx iff-term)]
+    (if (= status :ko)
+      (throw (ex-info "Cannot type term." {:special 'latte.prop/iff-elim-if%
+                                           :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]))))))
 
 (defthm iff-elim-only-if
   "Elimination rule for logical equivalence.

           H (not A)]
    (have a absurd :by (H x))
    (qed a)))


(definition truth
  "Logical truth."

    (qed <e>)))

(defthm or-sym
  "Symmetry of disjunction."
  [[A :type] [B :type]]
  (==> (or A B)
       (or B A)))
