Proof rule for the empty list of constraint.
Theorem: constraint-list-satp-of-nil
(defthm constraint-list-satp-of-nil (constraint-list-satp nil defs asg p))