                              <c> <d>)))
   (qed <e>))
 
-(defthm or-assoc-conv
+(defthm or-assoc-conv%
   [[A :type] [B :type] [C :type]]
   (==> (or A (or B C))
        (or (or A B) C)))
 
-(proof or-assoc-conv
+(proof 'or-assoc-conv%
     :script
   (assume [H1 (or A (or B C))]
     (assume [H2 A]
       (have <a1> (or A B)
-            :by (or-intro-left% H2 B))
+            :by (or-intro-left H2 B))
       (have <a> (or (or A B) C)
-            :by (or-intro-left% <a1> C)))
+            :by (or-intro-left <a1> C)))
     (assume [H3 (or B C)]
       (assume [H4 B]
         (have <b1> (or A B)
-              :by (or-intro-right% A H4))
+              :by (or-intro-right A H4))
         (have <b> (or (or A B) C)
-              :by (or-intro-left% <b1> C)))
+              :by (or-intro-left <b1> C)))
       (assume [H5 C]
         (have <c> (or (or A B) C)
-              :by (or-intro-right% (or A B) H5)))
+              :by (or-intro-right (or A B) H5)))
       (have <d> _
-            :by (or-elim% H3 (or (or A B) C)
+            :by (or-elim H3 (or (or A B) C)
                           <b> <c>)))
     (have <e> _
-          :by (or-elim% H1 (or (or A B) C)
+          :by (or-elim H1 (or (or A B) C)
                         <a> <d>)))
   (qed <e>))
 
-(defspecial or-assoc%
-  "Associativity of disjunction, a special that subsumes both
+(defimplicit or-assoc
+  "Associativity of disjunction, an implicit that subsumes both
 [[or-assoc]] and [[or-assoc-conv]]."
-  [def-env ctx or-term]
-  (let [[status ty] (ty/type-of-term def-env ctx or-term)]
-    (if (= status :ko)
-      (throw (ex-info "Cannot type term." {:special 'latte.prop/or-assoc%
-                                           :term or-term
-                                           :from ty}))
-      (let [[status A B] (decompose-or-type def-env ctx ty)]
-        (if (= status :ko)
-          (throw (ex-info "Not an `or`-type." {:special 'latte.prop/or-assoc%
-                                               :term or-term
-                                               :type ty}))
-          (let [[status A1 A2] (decompose-or-type def-env ctx A)]
-            (if (= status :ok)
-              [(list #'or-assoc A1 A2 B) or-term]
-              (let [[status B1 B2] (decompose-or-type def-env ctx B)]
-                (if (= status :ok)
-                  [(list #'or-assoc-conv A B1 B2) or-term]
-                  (throw (ex-info "Not an associative `or`-type."
-                                  {:special 'latte.prop/or-assoc%
-                                   :term or-term
-                                   :type ty})))))))))))
+  [def-env ctx [or-term or-type]]
+  (let [[A B] (decompose-or-type def-env ctx or-type)]
+    (try (let [[A1 A2] (decompose-or-type def-env ctx A)]
+           [(list #'or-assoc% A1 A2 B) or-term])
+         (catch Exception e
+           (let [[B1 B2] (decompose-or-type def-env ctx B)]
+             [(list #'or-assoc-conv% A B1 B2) or-term])))))
 
 (definition <=>
   "Logical equivalence or 'if and only if'."

    (have <e> B :by (<d> <b> <c>)))
  (qed <e>))

(defthm or-assoc
  [[A :type] [B :type] [C :type]]
  (==> (or (or A B) C)
       (or A (or B C))))

(proof 'or-assoc
    :script
  (assume [H1 (or (or A B)
                 C)]

  [[A :type]]
  (<=> A A))

(proof 'iff-refl
    :script
  (have <a> (==> A A) :by (impl-refl A))
  (have <b> (==> (==> A A)
                 (==> A A)
                 (<=> A A))
        :by (and-intro% (==> A A) (==> A A)))
  (have <c> (<=> A A) :by (<b> <a> <a>))
  (qed <c>))

(defthm iff-intro%
  "Introduction rule for logical equivalence."
  [[A :type] [B :type]]
  (==> (==> A B)
       (==> B A)
       (<=> A B)))

(proof 'iff-intro%
    :script
  (assume [H1 (==> A B)
           H2 (==> B A)]
    (have <a> (==> (==> A B)
                 (==> B A)
                 (<=> A B)) :by (and-intro% (==> A B) (==> B A)))
    (have <b> (<=> A B) :by (<a> H1 H2)))
  (qed <b>))

(defimplicit iff-intro
  "Introduction rule for logical equivalence, an implicit version of [[iff-intro%]]."
  [def-env ctx [ab ab-type] [ba ba-type]]
  (let [[A B] (decompose-impl-type def-env ctx ab-type)
        [B A'] (decompose-impl-type def-env ctx ba-type)]
    ;; XXX: check somethings on A' vs. A ?
    [[(list #'iff-intro% A B) ab] ba]))

(defthm iff-elim-if%
  "Elimination rule for logical equivalence.
   This one only keeps the if part of the equivalence."
  [[A :type] [B :type]]
  (==> (<=> A B)
       (==> A B)))

(proof 'iff-elim-if%
    :script
  (assume [H (<=> A B)]
    (have <a> (==> (<=> A B)
                 (==> A B))
          :by (and-elim-left% (==> A B) (==> B A)))
    (have <b> (==> A B) :by (<a> H)))
  (qed <b>))

(defn decompose-iff-type
  [def-env ctx t]
  (let [[L R] (decompose-and-type def-env ctx t)
        [A B] (decompose-impl-type def-env ctx L)]
    [A B]))

(defimplicit iff-elim-if
  "Left (if) elimination for `<=>`, an implicit version of [[iff-elim-if%]]."
  [def-env ctx [iff-term iff-type]]
  (let [[A B] (decompose-iff-type def-env ctx iff-type)]
    [(list #'iff-elim-if% A B) iff-term]))

(defthm iff-elim-only-if%
  "Elimination rule for logical equivalence.
   This one only keeps the only-if part of the equivalence."
  [[A :type] [B :type]]
  (==> (<=> A B)
       (==> B A)))

(proof 'iff-elim-only-if%
    :script
  (assume [H (<=> A B)]
    (have <a> (==> (<=> A B)
                 (==> B A))
          :by (and-elim-right% (==> A B) (==> B A)))
    (have <b> (==> B A) :by (<a> H)))
  (qed <b>))

(defimplicit iff-elim-only-if
  "Right (only if) elimination for `<=>`, an implicit version of [[iff-elim-only-if%]]."
  [def-env ctx [iff-term iff-type]]
  (let [[A B] (decompose-iff-type def-env ctx iff-type)]
    [(list #'iff-elim-only-if% A B) iff-term]))

(defthm iff-sym%
  "Symmetry of logical equivalence."
  [[A :type] [B :type]]
  (==> (<=> A B)
       (<=> B A)))

(proof 'iff-sym%
    :script
  (assume [H (<=> A B)]
    (have <a> (==> B A) :by (iff-elim-only-if H))
    (have <b> (==> A B) :by (iff-elim-if H))
    (have <c> (==> (==> B A)
                   (==> A B)
                   (<=> B A)) :by (iff-intro% B A))
    (have <d> (<=> B A) :by (<c> <a> <b>)))
    (qed <d>))

(defimplicit iff-sym
  "Symmetry of `<=>`, an implicit version of [[iff-sym]]."
  [def-env ctx [iff-term iff-type]]
  (let [[A B] (decompose-iff-type def-env ctx iff-type)]
    [(list #'iff-sym% A B) iff-term]))

(defthm iff-trans%
  "Transitivity of logical equivalence."
  [[A :type] [B :type] [C :type]]
  (==> (<=> A B)
       (<=> B C)
       (<=> A C)))

(proof 'iff-trans%
    :script
  (assume [H1 (<=> A B)
           H2 (<=> B C)]
    (have <a> (==> A B) :by (iff-elim-if H1))
    (have <b> (==> B C) :by (iff-elim-if H2))
    (have <c> _ :by (impl-trans% A B C))
    (have <d> (==> A C) :by (<c> <a> <b>))
    (have <e> (==> C B) :by (iff-elim-only-if H2))
    (have <f> (==> B A) :by (iff-elim-only-if H1))
    (have <g> _ :by (impl-trans% C B A))
    (have <h> (==> C A) :by (<g> <e> <f>))
    (have <i> _ :by (iff-intro% A C))
    (have <k> (<=> A C) :by (<i> <d> <h>)))
  (qed <k>))

(defimplicit iff-trans
  "Transitivity of `<=>`, an implicit version of [[iff-trans%]]."
  [def-env ctx [iff-term1 iff-type1] [iff-term2 iff-type2]]
  (let [[A B] (decompose-iff-type def-env ctx iff-type1)
        [C D] (decompose-iff-type def-env ctx iff-type2)]
    ;; XXX: check that B and C are equal ?
    [[(list #'iff-trans% A B D) iff-term1] iff-term2]))


