(tuplep n x) recognizes nil-terminated n-tuples.
Function: tuplep
(defun tuplep (n x) (declare (xargs :guard (natp n))) (mbe :logic (and (true-listp x) (equal (len x) n)) :exec (and (true-listp x) (eql (length x) n))))
