Description: Extend wff notation to include a predicate for standard models of a strong version of the Axiom Scheme of Replacement.