Turn a true list of doublets (i.e. lists of length 2) into the corresponding alist.
This is the inverse of alist-to-doublets.
(defun doublets-to-alist (doublets) (declare (xargs :guard (doublet-listp doublets))) (if (endp doublets) nil (cons (cons (car (first doublets)) (cadr (first doublets))) (doublets-to-alist (rest doublets)))))
(defthm doublets-to-alist-of-alist-to-doublets (implies (alistp x) (equal (doublets-to-alist (alist-to-doublets x)) x)))
(defthm alist-to-doublets-of-doublets-to-alist (implies (doublet-listp x) (equal (alist-to-doublets (doublets-to-alist x)) x)))