FGL binder that gets the constant-valued pairs from an alist.
(alist-const-pairs ans x) → *
Function:
(defun alist-const-pairs (ans x) (declare (xargs :guard t)) (let ((__function__ 'alist-const-pairs)) (declare (ignorable __function__)) (and (acl2::sub-alistp ans x) ans)))
Theorem:
(defthm sub-alistp-of-alist-const-pairs (acl2::sub-alistp (alist-const-pairs ans x) x))