Proof rule for the concatenation of lists of constraints.
Theorem:
(defthm constraint-list-satp-of-append (equal (constraint-list-satp (append constrs1 constrs2) defs asg p) (and (constraint-list-satp constrs1 defs asg p) (constraint-list-satp constrs2 defs asg p))))