     (have <b> (<=> (P y) (P x)) :by (p/iff-sym <a>)))
   (qed <b>))
 
-(defspecial eq-sym%
-  "Symmetry of equality, a special version of [[eq-sym]]."
-  [def-env ctx eq-term]
-  (let [[status ty] (ty/type-of-term def-env ctx eq-term)]
-    (if (= status :ko)
-      (throw (ex-info "Cannot type term." {:special 'latte.prop/eq-sym%
-                                           :term eq-term
-                                           :from ty}))
-      (do
-        (let [[status T x y] (decompose-equal-type def-env ctx ty)]
-          (if (= status :ko)
-            (throw (ex-info "Cannot infer an `equal`-type." {:special 'latte.prop/eq-sym%
-                                                             :term eq-term
-                                                             :type ty}))
-            [(list #'eq-sym T x y) eq-term]))))))
-
-(defthm eq-trans
+(defimplicit eq-sym
+  "Symmetry of equality, an implicit version of [[eq-sym%]]."
+  [def-env ctx [eq-term eq-ty]]
+  (let [[T x y] (decompose-equal-type def-env ctx eq-ty)]
+    [(list #'eq-sym% T x y) eq-term]))
+
+(defthm eq-trans%
   "The transitivity property of equality."
   [[T :type] [x T] [y T] [z T]]
-  (==> (equal T x y)
-       (equal T y z)
-       (equal T x z)))
-
-(proof eq-trans :script
-  (assume [H1 (equal T x y)
-           H2 (equal T y z)
+  (==> (equal% T x y)
+       (equal% T y z)
+       (equal% T x z)))
+
+(proof 'eq-trans% :script
+  (assume [H1 (equal x y)
+           H2 (equal y z)
            P (==> T :type)]
-    (have a (<=> (P x) (P y)) :by (H1 P))
-    (have b (<=> (P y) (P z)) :by (H2 P))
-    (have c (<=> (P x) (P z))
-          :by ((p/iff-trans (P x) (P y) (P z)) a b))
-    (qed c)))
-
-
-(defspecial eq-trans%
-  "Transitivity of `equal`, a special version of [[eq-trans]]."
-  [def-env ctx eq-term1 eq-term2]
-  (let [[status ty1] (ty/type-of-term def-env ctx eq-term1)]
-    (when (= status :ko)
-      (throw (ex-info "Cannot type term." {:special 'latte.prop/eq-trans%
-                                           :term eq-term1
-                                           :from ty1})))
-    (let [[status ty2] (ty/type-of-term def-env ctx eq-term2)]
-      (when (= status :ko)
-        (throw (ex-info "Cannot type term." {:special 'latte.prop/eq-trans%
-                                             :term eq-term2
-                                             :from ty2})))
-      (let [[status T1 x1 y1] (decompose-equal-type def-env ctx ty1)]
-        (when (= status :ko)
-          (throw (ex-info "Cannot infer an `equal`-type." {:special 'latte.prop/eq-trans%
-                                                           :term eq-term1
-                                                           :type ty1})))
-        (let [[status T2 x2 y2] (decompose-equal-type def-env ctx ty2)]
-          (when (= status :ko)
-            (throw (ex-info "Cannot infer an `equal`-type." {:special 'latte.prop/eq-trans%
-                                                             :term eq-term2
-                                                             :type ty2})))
-          ;; XXX: these are redundant and probably take time ...
-          #_(when-not (norm/beta-eq? def-env ctx T1 T2)
-            (throw (ex-info "Equal type mismatch"
-                            {:special 'latte.prop/eq-trans%
-                             :left-type T1
-                             :right-type T2})))
-          #_(when-not (norm/beta-eq? def-env ctx y1 x2)
-            (throw (ex-info "Term in the middle mismatch"
-                            {:special 'latte.prop/eq-trans%
-                             :left-rhs-term y1
-                             :right-lhs-term x2})))
-          [[(list #'eq-trans T1 x1 y1 y2) eq-term1] eq-term2])))))
-
-(defspecial eq-trans*
-  "Transitivity of `equal`, a n-ary version of [[eq-trans%]].
+    (have <a> (<=> (P x) (P y)) :by (H1 P))
+    (have <b> (<=> (P y) (P z)) :by (H2 P))
+    (have <c> (<=> (P x) (P z))
+          :by (p/iff-trans <a> <b>)))
+  (qed <c>))
+
+(defimplicit eq-trans
+  "Transitivity of `equal`, an implicit version of [[eq-trans%]]."
+  [def-env ctx [eq-term1 ty1] [eq-term2 ty2]]
+  (let [[T1 x1 y1] (decompose-equal-type def-env ctx ty1)
+        [T2 x2 y2] (decompose-equal-type def-env ctx ty2)]
+    ;; XXX: these are redundant and probably take time ...
+      #_(when-not (norm/beta-eq? def-env ctx T1 T2)
+          (throw (ex-info "Equal type mismatch"
+                          {:special 'latte.prop/eq-trans%
+                           :left-type T1
+                           :right-type T2})))
+      #_(when-not (norm/beta-eq? def-env ctx y1 x2)
+          (throw (ex-info "Term in the middle mismatch"
+                          {:special 'latte.prop/eq-trans%
+                           :left-rhs-term y1
+                           :right-lhs-term x2})))
+      [[(list #'eq-trans% T1 x1 y1 y2) eq-term1] eq-term2]))
+
+(defimplicit eq-trans*
+  "Transitivity of `equal`, a n-ary version of [[eq-trans]].
 The parameter `eq-terms` is a vector of at least two equalities.
 
 For example:
 
 ```
 (eq-trans* eq1 eq2)
-==> (eq-trans% eq1 eq2)
+==> (eq-trans eq1 eq2)
 
 (eq-trans* eq1 eq2 eq3)
-==> (eq-trans% (eq-trans% eq1 eq2) eq3)
+==> (eq-trans (eq-trans eq1 eq2) eq3)
 
 (eq-trans* eq1 eq2 eq3 eq4)
-==> (eq-trans% (eq-trans% (eq-trans% eq1 eq2) eq3) eq4)
+==> (eq-trans (eq-trans (eq-trans eq1 eq2) eq3) eq4)
 ````
 etc.
 `"

  (forall [P (==> T :type)]
    (<=> (P x) (P y))))


(defimplicit equal
  "Equality of `x` and `y` (which must be of the same type `T`).
This is an implicit version of [[equal%]]."

  ;;   (throw (ex-info "There must be at least two arguments."
  ;;                   {:special 'latte.prop/eq-trans*
  ;;                    :arg eq-terms})))
  (let [[T x1 y1] (decompose-equal-type def-env ctx (second (first eq-terms)))]
    (loop [eq-terms' (rest eq-terms), x1 x1, y1 y1, ret (ffirst eq-terms)]
      (if (seq eq-terms')
        (let [[_ x2 y2] (decompose-equal-type def-env ctx (second (first eq-terms')))]
          (recur (rest eq-terms') x1 y2
                 [[(list #'eq-trans% T x1 y1 y2) ret] (ffirst eq-terms')]))
        ;; we're done
        (do
          ;; (println "  ==> ret=" ret)
          ret)))))

;; (defthm test-eq-trans
;;   [[T :type] [a T] [b T] [c T] [d T]]
