Theorem:
(defthm svexlist-ovcongruent-necc (implies (svexlist-ovcongruent x) (implies (svex-envs-ovsimilar env1 env2) (equal (equal (svexlist-eval x env1) (svexlist-eval x env2)) t))))
Theorem:
(defthm svexlist-eval-equiv-implies-equal-svexlist-ovcongruent-1 (implies (svexlist-eval-equiv x x-equiv) (equal (svexlist-ovcongruent x) (svexlist-ovcongruent x-equiv))) :rule-classes (:congruence))