Proof rule for a cons list of constraints.
The satisfaction of a cons list of constraints reduces to the satisfaction of the two constituents (the first constraint and the remaining list).
This is a key proof rule to decompose the satisfaction of lists of constraints into the satisfaction of their constituent constraints.
Theorem:
(defthm constraint-list-satp-of-cons (equal (constraint-list-satp (cons constr constrs) defs asg p) (and (constraint-satp constr defs asg p) (constraint-list-satp constrs defs asg p))))