We interpret additional predicates before the turnstile. These simply express validity in a sub-universe. This means that for any sound rule the corresponding rule with additional predicates is also sound.