   ;;   (throw (ex-info "There must be at least two arguments."
   ;;                   {:special 'latte.prop/eq-trans*
   ;;                    :arg eq-terms})))
-  (let [[status ty1] (ty/type-of-term def-env ctx (first eq-terms))]
-    (when (= status :ko)
-      (throw (ex-info "Cannot type term." {:special 'latte.prop/eq-trans*
-                                           :term (first eq-terms)
-                                           :from ty1})))
-    (let [[status T 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 (first eq-terms)
-                                                         :type ty1})))
-      (loop [eq-terms' (rest eq-terms), x1 x1, y1 y1, ret (first eq-terms)]
-        (if (seq eq-terms')
-          (let [[status ty2] (ty/type-of-term def-env ctx (first eq-terms'))]
-            (when (= status :ko)
-              (throw (ex-info "Cannot type term." {:special 'latte.prop/eq-trans*
-                                                   :term (first eq-terms')
-                                                   :from ty2})))
-            (let [[status _ 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 (first eq-terms')
-                                                                 :type ty2})))
-              (recur (rest eq-terms') x1 y2
-                     [[(list #'eq-trans T x1 y1 y2) ret] (first eq-terms')])))
-          ;; we're done
-          (do
-            ;; (println "  ==> ret=" ret)
-            ret))))))
+  (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]]

  (list #'equal% x-ty x y))

(defn decompose-equal-type [def-env ctx t]
  (if (clojure.core/and (seq t)
                        (= (count t) 4)
                        (= (first t) #'latte.equal/equal%))
    [(second t) (nth t 2) (nth t 3)]
    (let [[t ok?] (norm/delta-step def-env t)]
      ;; (println "[decompose-equal-type] delta-term=" t " (reduced ? " ok? ")")
      (if ok?
        (recur def-env ctx t)
        (let [[t ok?] (norm/beta-step t)]
          (if ok?
            (recur def-env ctx t)
            ;; XXX: cannot decompose further because
            ;; we cannot retrieve the x and y of the
            ;; definition ... add dummy witnesses ?
            (throw (ex-info "Cannot infer an equal-type" {:type t}))))))))

(defthm eq-refl%
  "The reflexivity property of equality."


(defimplicit eq-refl
  "Equality is reflexive."
  [def-env ctx [x x-ty]]
  (list #'eq-refl% x-ty x x))

(defthm eq-sym%
  "The symmetry property of equality."
