fact: Definition models (φ ψ0 ψ1: valuation) : constraint -> Prop := fun '((a, x), (y, b)) => match φ y with | atom _ => False | arr s t => (if b then t else s) = substitute (if a then ψ1 else ψ0) (φ x) end.
imports: List