Theorem:
(defthm svexlist-eval-equiv-implies-equal-svexlist-monotonic-p-1 (implies (svexlist-eval-equiv x x-equiv) (equal (svexlist-monotonic-p x) (svexlist-monotonic-p x-equiv))) :rule-classes (:congruence))
Theorem:
(defthm svex-monotonic-p-of-car-when-svexlist-monotonic-p (implies (svexlist-monotonic-p x) (svex-monotonic-p (car x))))
Theorem:
(defthm svexlist-monotonic-p-of-cdr-when-svexlist-monotonic-p (implies (svexlist-monotonic-p x) (svexlist-monotonic-p (cdr x))))
Theorem:
(defthm svex-monotonic-p-of-nth-when-svexlist-monotonic-p (implies (svexlist-monotonic-p x) (svex-monotonic-p (nth n x))))