Basic theorems about faig-fix-alist.
Theorem:
(defthm hons-assoc-equal-faig-fix-alist (equal (hons-assoc-equal x (faig-fix-alist a)) (and (hons-assoc-equal x a) (cons x (faig-fix (cdr (hons-assoc-equal x a)))))))
Theorem:
(defthm faig-restrict-alist-faig-fix-alist (equal (faig-restrict-alist (faig-fix-alist a) env) (faig-restrict-alist a env)))
Theorem:
(defthm faig-partial-eval-alist-faig-fix-alist (equal (faig-partial-eval-alist (faig-fix-alist a) env) (faig-partial-eval-alist a env)))