   (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%]]."


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

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

  ;;   (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]]
