Proof rule for a reversed list of constraints.
Theorem: constraint-list-satp-of-rev
(defthm constraint-list-satp-of-rev (equal (constraint-list-satp (rev constrs) defs asg p) (constraint-list-satp constrs defs asg p)))