Implement formulae parametrized by atomic predicates.