Basic theorems about svexlist-vars.
Theorem:
(defthm svexlist-vars-of-cons (set-equiv (svexlist-vars (cons a b)) (append (svex-vars a) (svexlist-vars b))))
Theorem:
(defthm svexlist-vars-of-append (equal (svexlist-vars (append x y)) (union (svexlist-vars x) (svexlist-vars y))))
Theorem:
(defthm svex-vars-subset-of-svexlist-vars-when-member (implies (member x y) (subsetp (svex-vars x) (svexlist-vars y))))
Theorem:
(defthm svexlist-vars-of-subset (implies (subsetp x y) (subsetp (svexlist-vars x) (svexlist-vars y))))
Theorem:
(defthm set-equiv-implies-equal-svexlist-vars-1 (implies (set-equiv x x-equiv) (equal (svexlist-vars x) (svexlist-vars x-equiv))) :rule-classes (:congruence))