Introduce

Heim and Kratzer's "Predicate Abstraction Rule"