A macro for defining universally quantified equivalence relations.

It is often useful to introduce equivalence relations such as:

A === B when for every possible element E, A and B agree on E.

For some particular notion of what *agree* means. This macro gives you
a quick way to introduce such a relation, using defun-sk, and then
automatically prove that it is an equivalence relation. For instance, an
equivalence such as:

(defun-sk foo-equiv (a b) (forall (x y z) (and (bar-equiv (foo a x y) (foo b x y)) (baz-equiv (fa a z) (fa b z)))))

Can be introduced using:

(def-universal-equiv foo-equiv (a b) :qvars (x y z) :equivs ((bar-equiv (foo a x y)) (baz-equiv (fa a z))))

When called with

Note that

(def-universal-equiv gfix-equiv :equiv-terms ((equal (gfix x))))

produces

(defun gfix-equiv (x y) (equal (gfix x) (gfix y))) (defequiv gfix-equiv)

(with appropriate hints to ensure that the