Try to find a key for which two four-valued alists don't agree.
Function:
(defun 4v-alists-disagree-witness (keys al1 al2) (declare (xargs :guard t)) (if (atom keys) nil (if (equal (4v-lookup (car keys) al1) (4v-lookup (car keys) al2)) (4v-alists-disagree-witness (cdr keys) al1 al2) (car keys))))
Theorem:
(defthm 4v-alists-witness-correct (iff (4v-alists-agree keys al1 al2) (let ((witness (4v-alists-disagree-witness keys al1 al2))) (or (not (member-equal witness keys)) (equal (4v-lookup witness al1) (4v-lookup witness al2))))))