## DEFCONG

prove that one equivalence relation preserves another in a given
` `

argument position of a given function
Major Section: EVENTS

Example:
(defcong set-equal iff (memb x y) 2)
is an abbreviation for
(defthm set-equal-implies-iff-memb-2
(implies (set-equal y y-equiv)
(iff (memb x y) (memb x y-equiv)))
:rule-classes (:congruence))

See congruence and also see equivalence.

General Form:
(defcong equiv1 equiv2 term k
:rule-classes rule-classes
:instructions instructions
:hints hints
:otf-flg otf-flg
:event-name event-name
:doc doc)

where `equiv1`

and `equiv2`

are known equivalence relations, `term`

is a
call of a function `fn`

on the correct number of distinct variable
arguments `(fn x1 ... xn)`

, `k`

is a positive integer less than or equal
to the arity of `fn`

, and other arguments are as specified in the
documentation for `defthm`

. The `defcong`

macro expands into a call
of `defthm`

. The name of the `defthm`

event is
`equiv1-implies-equiv2-fn-k`

unless an `:event-name`

keyword argument is
supplied for the name. The term of the theorem is
(implies (equiv1 xk yk)
(equiv2 (fn x1... xk ...xn)
(fn x1... yk ...xn))).

The rule-class `:`

`congruence`

is added to the `rule-classes`

specified,
if it is not already there. All other arguments to the generated
`defthm`

form are as specified by the keyword arguments above.