Theorem:
(defthm svexlist-ovmonotonic-necc (implies (svexlist-ovmonotonic x) (implies (svex-env-ov<<= env1 env2) (4veclist-<<= (svexlist-eval x env1) (svexlist-eval x env2)))))
Theorem:
(defthm svexlist-eval-equiv-implies-equal-svexlist-ovmonotonic-1 (implies (svexlist-eval-equiv x x-equiv) (equal (svexlist-ovmonotonic x) (svexlist-ovmonotonic x-equiv))) :rule-classes (:congruence))