Proof rule for relation application constraints, for the case in which the relation has no free variables.
This is a specialized version of constraint-satp-of-relation, applicable when the definition of the relation has no free variables. In this case, we can rewrite the satisfaction to the function constraint-relation-nofreevars-satp, which avoids the existential quantification.
Theorem:
(defthm constraint-satp-of-relation-when-nofreevars (implies (and (assignmentp asg) (assignment-wfp asg p) (constraint-case constr :relation)) (b* ((name (constraint-relation->name constr)) (args (constraint-relation->args constr)) (def (lookup-definition name defs))) (implies (and def (emptyp (definition-free-vars def))) (equal (constraint-satp constr defs asg p) (constraint-relation-nofreevars-satp name args defs asg p))))))